Require Import RingLike.Polynomial_algebra.

From Stdlib Require Import Utf8 Arith.
Import List.ListNotations Init.Nat.

Require Import Core Misc Utils.
Require Import IterAdd.
Require Import Lap_algebra.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.

Theorem strip_0s_idemp : ∀ la, strip_0s (strip_0s la) = strip_0s la.

Definition lap_psub la lb :=
  List_map2 rngl_psub
    (la ++ List.repeat 0%L (length lb - length la))
    (lb ++ List.repeat 0%L (length la - length lb)).

Definition lap_opp la := List.map rngl_opp la.

Definition lap_sub la lb :=
  if rngl_has_opp T then lap_add la (lap_opp lb)
  else if rngl_has_psub T then lap_psub la lb
  else List.repeat 0%L (max (length la) (length lb)).

Theorem fold_lap_psub :
  ∀ la lb,
  List_map2 rngl_psub (la ++ List.repeat 0%L (length lb - length la))
    (lb ++ List.repeat 0%L (length la - length lb)) =
  lap_psub la lb.

Theorem fold_lap_opp : ∀ la, List.map rngl_opp la = lap_opp la.

Theorem fold_lap_norm : ∀ la, List.rev (strip_0s (List.rev la)) = lap_norm la.


Definition rlap_pdiv_rem_nb_iter (la lb : list T) :=
  S (length la).

Definition rlap_pdiv_rem_step (rla rlb : list T) :=
  match rlb with
  | [] ⇒ (None, [])
  | b :: rlb' ⇒
      match rla with
      | [] ⇒ (None, [])
      | a :: rla' ⇒
          if length rla' <? length rlb' then (None, rla)
          else
            let cq := (a / b)%L in
            let rlr := lap_sub rla' (List.map (λ cb, (cb × cq)%L) rlb') in
            (Some cq, rlr)
      end
  end.

Fixpoint rlap_pdiv_rem_loop it (rla rlb : list T) : list T × list T :=
  match it with
  | 0 ⇒ ([], [rngl_of_nat 97])
  | S it' ⇒
      let (q, rlr) := rlap_pdiv_rem_step rla rlb in
      match q with
      | Some cq ⇒
           let (rlq', rlr') := rlap_pdiv_rem_loop it' rlr rlb in
           (cq :: rlq', rlr')
      | None ⇒ ([], rlr)
      end
  end.

Definition rlap_pdiv_rem rla rlb :=
  rlap_pdiv_rem_loop (rlap_pdiv_rem_nb_iter rla rlb) rla rlb.

Definition lap_pdiv_rem la lb :=
  let (rlq, rlr) := rlap_pdiv_rem (List.rev la) (List.rev lb) in
  (List.rev rlq, List.rev (strip_0s rlr)).

Definition lap_pdiv la lb :=
  let (rlq, rlr) := rlap_pdiv_rem (List.rev la) (List.rev lb) in
  List.rev rlq.

Definition lap_rem la lb :=
  let (rlq, rlr) := rlap_pdiv_rem (List.rev la) (List.rev lb) in
  List.rev (strip_0s rlr).

End a.

Arguments lap_psub {T ro} (la lb)%_lap.

Notation "- a" := (lap_opp a) : lap_scope.
Notation "a - b" := (lap_sub a b) : lap_scope.
Notation "a / b" := (lap_pdiv a b) : lap_scope.
Notation "a 'mod' b" := (lap_rem a b) : lap_scope.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context (Hos : rngl_has_opp_or_psub T = true).
Context (Hed : rngl_has_eq_dec T = true).

Theorem List_map2_rngl_psub_0_r :
  rngl_has_psub T = true →
  ∀ n la,
  n = length la
  → List_map2 rngl_psub la (List.repeat 0%L n) = la.

Theorem lap_psub_0_r :
  rngl_has_psub T = true →
  ∀ la, lap_psub la 0 = la.


Theorem strip_0s_length_le : ∀ l, length (strip_0s l) ≤ length l.

Theorem lap_psub_length : ∀ la lb,
  length (lap_psub la lb) = max (length la) (length lb).

Theorem lap_opp_length : ∀ la, length (- la)%lap = length la.

Theorem lap_sub_length : ∀ la lb,
  length (la - lb)%lap = max (length la) (length lb).


Theorem rlap_pdiv_rem_step_None : ∀ la lb lr,
  rlap_pdiv_rem_step la lb = (None, lr)
  → lb = [] ∧ lr = [] ∨ la = [] ∧ lr = [] ∨ length la < length lb ∧ lr = la.

Theorem rlap_pdiv_rem_step_length_r_a : ∀ rla rlb rlr cq,
  rlap_pdiv_rem_step rla rlb = (Some cq, rlr)
  → S (length rlr) = length rla.

Theorem rlap_rem_loop_prop : ∀ it rla rlb rlq rlr,
  rlb ≠ []
  → rlap_pdiv_rem_loop it rla rlb = (rlq, rlr)
  → S (length rla) ≤ it
  → length rlr < length rlb.

Theorem lap_mul_length : ∀ la lb,
  length (la × lb)%lap =
    match length la with
    | 0 ⇒ 0
    | S a ⇒
        match length lb with
        | 0 ⇒ 0
        | S b ⇒ S (a + b)
        end
    end.

Theorem lap_norm_List_map2_app_app_idemp_r :
  ∀ f, (∀ a, f a 0%L = a) →
  ∀ la lb,
  lap_norm
    (List_map2 f (la ++ List.repeat 0%L (length (lap_norm lb) - length la))
       (lap_norm lb ++ List.repeat 0%L (length la - length (lap_norm lb)))) =
  lap_norm
    (List_map2 f (la ++ List.repeat 0%L (length lb - length la))
       (lb ++ List.repeat 0%L (length la - length lb))).


Theorem lap_psub_norm_idemp_l :
  rngl_has_psub T = true →
  ∀ la lb,
  lap_norm (lap_psub (lap_norm la) lb) = lap_norm (lap_psub la lb).

Theorem lap_psub_norm_idemp_r :
  rngl_has_psub T = true →
  ∀ la lb,
  lap_norm (lap_psub la (lap_norm lb)) = lap_norm (lap_psub la lb).


Theorem lap_mul_1_l :
  ∀ la, (1 × la)%lap = la.

Theorem lap_mul_1_r :
  ∀ la, (la × 1)%lap = la.


Theorem last_lap_convol_mul_last :
  ∀ la lb a b i len d,
  len ≠ 0
  → length la + length lb + 1 = i + len
  → List.last (lap_convol_mul (la ++ [a]) (lb ++ [b]) i len) d = (a × b)%L.

Theorem last_lap_mul :
  ∀ la lb, List.last (la × lb)%lap 0%L = (List.last la 0 × List.last lb 0)%L.


Theorem List_map2_rngl_psub_diag :
  ∀ la, List_map2 rngl_psub la la = List.repeat 0%L (length la).

Theorem lap_opt_add_sub :
  rngl_has_psub T = true →
  ∀ la lb : list T,
  (la + lb - lb)%lap = la ++ List.repeat 0%L (length lb - length la).
Theorem lap_psub_add_distr :
  rngl_has_psub T = true →
  ∀ la lb lc, lap_psub la (lb + lc) = lap_psub (lap_psub la lb) lc.

Theorem lap_opt_sub_add_distr :
  rngl_has_psub T = true →
  ∀ la lb lc : list T, (la - (lb + lc))%lap = (la - lb - lc)%lap.


Theorem lap_mul_opp_r :
  rngl_has_opp T = true →
  ∀ la lb, (la × - lb = - (la × lb))%lap.

Theorem lap_mul_sub_distr_l :
  rngl_has_opp T = true →
  ∀ la lb lc, (la × (lb - lc))%lap = (la × lb - la × lc)%lap.


Definition is_empty_list {A} (la : list A) :=
  match la with [] ⇒ true | _ ⇒ false end.
Definition has_polyn_prop {T} {ro : ring_like_op T} (la : list T) :=
  (is_empty_list la || (List.last la 0 ≠? 0)%L)%bool.

Theorem rlap_rem_prop : ∀ rla rlb rlq rlr,
  rlb ≠ []
  → rlap_pdiv_rem rla rlb = (rlq, rlr)
  → List.length rlr < List.length rlb.

Theorem lap_rem_length_lt :
  ∀ la lb lq lr : list T,
  lb ≠ []
  → has_polyn_prop lb = true
  → lap_pdiv_rem la lb = (lq, lr)
  → List.length lr < List.length lb.

Theorem is_empty_list_empty : ∀ A (la : list A),
  is_empty_list la = true → la = [].

Theorem rlap_pdiv_prop :
  rngl_has_inv T = true →
  ∀ la lb lq lr,
  la = [] ∨ List.hd 0%L la ≠ 0%L
  → lb = [] ∨ List.hd 0%L lb ≠ 0%L
  → rlap_pdiv_rem la lb = (lq, lr)
  → lq = [] ∨ List.hd 0%L lq ≠ 0%L.

Theorem lap_convol_mul_1_l :
  ∀ la i len,
  List.length la = i + len
  → lap_convol_mul [1%L] la i len = List.skipn i la.

Theorem lap_convol_mul_l_succ_l :
  ∀ la lb i len,
  lap_convol_mul (0%L :: la) lb (S i) len =
  lap_convol_mul la lb i len.

Definition lap_x_power n := List.repeat 0%L n ++ [1%L].

Theorem lap_repeat_0_app_is_mul_power_l :
  ∀ n la,
  la ≠ []
  → List.repeat 0%L n ++ la = (lap_x_power n × la)%lap.

Theorem lap_convol_mul_1_r :
  ∀ la i len,
  List.length la = i + len
  → lap_convol_mul la [1%L] i len = List.skipn i la.

Theorem lap_convol_mul_r_succ_l :
  ∀ la lb i len,
  lap_convol_mul la (0%L :: lb) (S i) len =
  lap_convol_mul la lb i len.

Theorem lap_repeat_0_app_is_mul_power_r :
  ∀ n la,
  la ≠ []
  → List.repeat 0%L n ++ la = (la × lap_x_power n)%lap.

Theorem lap_add_repeat_0_l : ∀ la len,
  len ≤ List.length la
  → (List.repeat 0%L len + la = la)%lap.

Theorem lap_add_repeat_0_r : ∀ la len,
  len ≤ List.length la
  → (la + List.repeat 0%L len = la)%lap.

Theorem lap_add_app_app :
  ∀ la lb lc ld,
  List.length la = List.length lb
  → ((la ++ lc) + (lb ++ ld))%lap = (la + lb)%lap ++ (lc + ld)%lap.

Theorem rev_lap_add : ∀ la lb,
  List.length la = List.length lb
  → (List.rev (la + lb) = List.rev la + List.rev lb)%lap.

Theorem lap_add_norm : ∀ la lb,
  (la + lb)%lap =
    ((la ++ List.repeat 0%L (List.length lb - List.length la)) +
     (lb ++ List.repeat 0%L (List.length la - List.length lb)))%lap.

Theorem rev_lap_add_norm : ∀ la lb,
  List.rev (la + lb)%lap =
    ((List.repeat 0%L (List.length lb - List.length la) ++ List.rev la) +
     (List.repeat 0%L (List.length la - List.length lb) ++ List.rev lb))%lap.
Theorem lap_opp_app_distr : ∀ la lb,
  (- (la ++ lb) = (- la) ++ (- lb))%lap.

Theorem rev_lap_opp : ∀ la, (List.rev (- la) = - List.rev la)%lap.

Theorem map_opp_repeat : ∀ (x : T) n,
  List.map rngl_opp (List.repeat x n) = List.repeat (rngl_opp x) n.

Theorem rev_lap_sub : ∀ la lb,
  List.length la = List.length lb
  → (List.rev (la - lb) = List.rev la - List.rev lb)%lap.

Theorem lap_add_app_l : ∀ la lb lc,
  List.length lc ≤ List.length la
  → (((la ++ lb) + lc) = (la + lc) ++ lb)%lap.

Theorem lap_add_opp_diag_l :
  rngl_has_opp T = true
  → ∀ la, (- la + la)%lap = List.repeat 0%L (List.length la).

Theorem lap_sub_add :
  rngl_has_opp T = true →
  ∀ la lb,
  List.length lb ≤ List.length la
  → (la - lb + lb = la)%lap.

Theorem rev_lap_sub_norm :
  ∀ la lb,
  List.rev (la - lb)%lap =
    ((List.repeat 0%L (List.length lb - List.length la) ++ List.rev la) -
     (List.repeat 0%L (List.length la - List.length lb) ++ List.rev lb))%lap.

Theorem rlap_pdiv_rem_step_Some :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ rla rlb rlr cq,
  List.hd 0%L rlb ≠ 0%L
  → rlap_pdiv_rem_step rla rlb = (Some cq, rlr)
  → List.rev rla =
      (List.rev rlb ×
         List.rev
           (cq :: List.repeat 0%L (List.length rla - List.length rlb)) +
       List.rev rlr)%lap ∧
    List.length rla = S (List.length rlr) ∧
    cq = (List.hd 0 rla / List.hd 0 rlb)%L.

Theorem rlap_pdiv_rem_length :
  ∀ {it} {rla rlb : list T} rlq rlr,
  List.hd 0%L rlb ≠ 0%L
  → rlap_pdiv_rem_loop it rla rlb = (rlq, rlr)
  → S (List.length rla) ≤ it
  → List.length rlq = List.length rla - (List.length rlb - 1).

Theorem lap_add_app_r : ∀ la lb lc,
  List.length la ≤ List.length lb
  → (la + (lb ++ lc) = (la + lb) ++ lc)%lap.

Theorem rlap_pdiv_rem_loop_prop :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ it (rla rlb rlq rlr : list T),
  List.hd 0%L rlb ≠ 0%L
  → rlap_pdiv_rem_loop it rla rlb = (rlq, rlr)
  → S (List.length rla) ≤ it
  → List.rev rla = (List.rev rlb × List.rev rlq + List.rev rlr)%lap.

Theorem all_0_all_rev_0 : ∀ A (d a : A) la,
  (∀ i, i < List.length la → List.nth i la d = a)
  ↔ (∀ i, i < List.length la → List.nth i (List.rev la) d = a).
Theorem eq_strip_0s_nil : ∀ d la,
  strip_0s la = [] ↔ ∀ i, i < length la → List.nth i la d = 0%L.
Theorem eq_strip_0s_rev_nil : ∀ la,
  strip_0s (List.rev la) = [] ↔
    ∀ i, i < List.length la → List.nth i la 0%L = 0%L.
Theorem lap_add_rev_strip : ∀ la lb,
  List.length lb ≤ List.length la
  → (la + List.rev (strip_0s lb) = la + List.rev lb)%lap.

Theorem lap_div_mod :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ la lb lq lr : list T,
  has_polyn_prop la = true
  → List.last lb 0%L ≠ 0%L
  → has_polyn_prop lr = true
  → lap_pdiv_rem la lb = (lq, lr)
  → la = (lb × lq + lr)%lap ∧
    List.length lr < List.length lb ∧
    has_polyn_prop lq = true.

Arguments lap_pdiv_rem {T ro} (la lb)%_lap.

Theorem eq_strip_0s_cons : ∀ la lb b,
  strip_0s la = b :: lb
  → b ≠ 0%L ∧
    ∃ i,
    i < length la ∧
    (∀ j, j < i → List.nth j la 0%L = 0%L) ∧
    List.nth i la 0%L = b.

Theorem polyn_norm_prop : ∀ la, has_polyn_prop (lap_norm la) = true.

Theorem all_0_lap_norm_nil : ∀ la,
  (∀ i, List.nth i la 0%L = 0%L)
  ↔ lap_norm la = [].
Theorem lap_norm_app_repeat_0 : ∀ la,
  la =
    lap_norm la ++
    List.repeat 0%L (List.length la - List.length (lap_norm la)).
Theorem lap_norm_length_le : ∀ la, List.length (lap_norm la) ≤ List.length la.

Theorem lap_pdiv_is_norm :
  rngl_has_inv T = true →
  ∀ la lb,
  has_polyn_prop la = true
  → has_polyn_prop lb = true
  → has_polyn_prop (lap_pdiv la lb) = true.

Theorem lap_rem_is_norm : ∀ la lb,
  has_polyn_prop la = true
  → has_polyn_prop lb = true
  → has_polyn_prop (lap_rem la lb) = true.


Theorem has_polyn_prop_lap_norm : ∀ la,
  has_polyn_prop la = true
  → lap_norm la = la.

Theorem lap_convol_mul_0_l : ∀ la lb i len,
  (∀ i, List.nth i la 0%L = 0%L)
  → lap_norm (lap_convol_mul la lb i len) = [].

Theorem lap_convol_mul_0_r : ∀ la lb i len,
  (∀ i, List.nth i lb 0%L = 0%L)
  → lap_norm (lap_convol_mul la lb i len) = [].

Theorem lap_convol_mul_cons_with_0_l : ∀ a la lb i len,
  (∀ i, List.nth i la 0%L = 0%L)
  → lap_convol_mul (a :: la) lb i len = lap_convol_mul [a] lb i len.

Theorem lap_convol_mul_app_rep_0_l : ∀ la lb i len n,
  lap_norm (lap_convol_mul (la ++ List.repeat 0%L n) lb i len) =
  lap_norm (lap_convol_mul la lb i len).
Theorem lap_convol_mul_app_rep_0_r : ∀ la lb i len n,
  lap_norm (lap_convol_mul la (lb ++ List.repeat 0%L n) i len) =
  lap_norm (lap_convol_mul la lb i len).
Theorem lap_norm_convol_mul_norm_r : ∀ la lb i len,
  lap_norm (lap_convol_mul la (lap_norm lb) i len) =
  lap_norm (lap_convol_mul la lb i len).

Theorem lap_norm_cons_norm : ∀ a la lb i len,
  List.length (a :: la) + List.length lb - 1 ≤ i + len
  → lap_norm (lap_convol_mul (a :: lap_norm la) lb i len) =
    lap_norm (lap_convol_mul (a :: la) lb i len).

Theorem lap_mul_norm_idemp_l : ∀ la lb,
  lap_norm (lap_norm la × lb)%lap = lap_norm (la × lb)%lap.

Theorem lap_mul_norm_idemp_r : ∀ la lb,
  lap_norm (la × lap_norm lb)%lap = lap_norm (la × lb)%lap.

Theorem list_nth_lap_opp :
  rngl_has_opp T = true →
  ∀ k la, (List.nth k (lap_opp la) 0 = - List.nth k la 0)%L.

Theorem list_nth_lap_sub :
  rngl_has_opp T = true →
  ∀ k la lb,
  (List.nth k (lap_sub la lb) 0 =
   List.nth k la 0 - List.nth k lb 0)%L.

Theorem lap_add_opp_diag_r :
  rngl_has_opp T = true
  → ∀ la, (la + - la)%lap = List.repeat 0%L (List.length la).

Theorem lap_norm_repeat_0 : ∀ n, lap_norm (List.repeat 0%L n) = [].

Theorem lap_norm_add_opp_diag_l :
  rngl_has_opp T = true
  → ∀ la, lap_norm (- la + la)%lap = [].


Theorem lap_psub_diag :
  ∀ la, lap_psub la la = List.repeat 0%L (List.length la).

Theorem lap_add_sub :
  ∀ la lb,
  (la + lb - lb)%lap =
    la ++ List.repeat 0%L (List.length lb - List.length la).

Theorem lap_add_move_l :
  ∀ la lb lc : list T,
  (la + lb)%lap = lc
  → lb ++ List.repeat 0%L (List.length la - List.length lb) = (lc - la)%lap.

Theorem lap_mul_has_polyn_prop :
  rngl_has_inv T = true →
  ∀ la lb,
  has_polyn_prop la = true
  → has_polyn_prop lb = true
  → has_polyn_prop (la × lb)%lap = true.

Theorem lap_norm_mul :
  rngl_has_inv T = true →
  ∀ la lb,
  has_polyn_prop la = true
  → has_polyn_prop lb = true
  → lap_norm (la × lb) = (la × lb)%lap.

Theorem lap_mul_div :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ la lb,
  has_polyn_prop la = true
  → has_polyn_prop lb = true
  → lb ≠ []
  → (la × lb / lb)%lap = la.

Let Heo := rngl_has_eq_dec_or_is_ordered_l Hed.

Theorem lap_rngl_of_nat :
  let lop := lap_ring_like_op Heo in
  ∀ n, rngl_of_nat n = if Nat.eq_dec n 0 then [] else [rngl_of_nat n].

End a.


Record polyn T {ro : ring_like_op T} := mk_polyn
  { lap : list T;
    lap_prop : has_polyn_prop lap = true }.

Arguments mk_polyn {T ro} lap%_lap.
Arguments lap {T ro}.
Arguments lap_prop {T ro}.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context (Hos : rngl_has_opp_or_psub T = true).
Context (Hed : rngl_has_eq_dec T = true).


Theorem eq_polyn_eq : ∀ pa pb,
  lap pa = lap pb
  ↔ pa = pb.

Theorem polyn_eq_dec : ∀ P Q : polyn T, {P = Q} + {P ≠ Q}.
Definition polyn_of_norm_lap la :=
  mk_polyn (lap_norm la) (polyn_norm_prop la).

Definition polyn_of_const c :=
  polyn_of_norm_lap [c].

Arguments polyn_of_const c%_L.

Definition polyn_zero := mk_polyn [] eq_refl.
Definition polyn_one := polyn_of_const 1.

Definition polyn_norm la := mk_polyn (lap_norm la) (polyn_norm_prop la).
Definition polyn_add p1 p2 := polyn_norm (lap_add (lap p1) (lap p2)).
Definition polyn_opp pol := polyn_norm (lap_opp (lap pol)).

Definition polyn_psub p1 p2 := polyn_norm (lap_psub (lap p1) (lap p2)).

Definition polyn_mul p1 p2 := polyn_norm (lap_mul (lap p1) (lap p2)).

Definition polyn_pdiv (pa pb : polyn T) : polyn T :=
  match Sumbool.sumbool_of_bool (rngl_has_inv T) with
  | left Hiv ⇒
      let lq := lap_pdiv (lap pa) (lap pb) in
      mk_polyn lq
        (lap_pdiv_is_norm Hos Hed Hiv (lap pa) (lap pb) (lap_prop pa)
           (lap_prop pb))
  | right _ ⇒
      polyn_zero
  end.


Definition polyn_opt_opp_or_psub :
  option ((polyn T → polyn T) + (polyn T → polyn T → polyn T)) :=
  match rngl_opt_opp_or_psub T with
  | Some (inl _) ⇒ Some (inl polyn_opp)
  | Some (inr _) ⇒ Some (inr polyn_psub)
  | None ⇒ None
  end.


Definition polyn_opt_inv_or_pdiv :
  option ((polyn T → polyn T) + (polyn T → polyn T → polyn T)) :=
  match Sumbool.sumbool_of_bool (rngl_mul_is_comm T) with
  | left Hco ⇒
      match Sumbool.sumbool_of_bool (rngl_has_opp T) with
      | left Hop ⇒
          match Sumbool.sumbool_of_bool (rngl_has_inv T) with
         | left Hiv ⇒
             match rngl_opt_inv_or_pdiv T with
             | Some _ ⇒ Some (inr polyn_pdiv)
             | None ⇒ None
             end
          | right _ ⇒ None
          end
      | right _ ⇒ None
      end
  | right _ ⇒ None
  end.

Definition polyn_ring_like_op : ring_like_op (polyn T) :=
  {| rngl_zero := polyn_zero;
     rngl_one := polyn_one;
     rngl_add := polyn_add;
     rngl_mul := polyn_mul;
     rngl_opt_opp_or_psub := polyn_opt_opp_or_psub;
     rngl_opt_inv_or_pdiv := polyn_opt_inv_or_pdiv;
     rngl_opt_is_zero_divisor := Some (λ _, True);
     rngl_opt_eq_dec := Some polyn_eq_dec;
     rngl_opt_leb := None |}.



Declare Scope polyn_scope.
Delimit Scope polyn_scope with pol.

Notation "0" := polyn_zero : polyn_scope.
Notation "1" := polyn_one : polyn_scope.
Notation "- a" := (polyn_opp a) : polyn_scope.
Notation "a + b" := (polyn_add a b) : polyn_scope.
Notation "a * b" := (polyn_mul a b) : polyn_scope.

Theorem polyn_add_comm :
  let rop := polyn_ring_like_op in
  ∀ a b : polyn T, (a + b)%L = (b + a)%L.

Theorem polyn_add_assoc : ∀ pa pb pc,
  (pa + (pb + pc) = (pa + pb) + pc)%pol.

Theorem polyn_add_0_l : ∀ p, (0 + p)%pol = p.

Theorem polyn_mul_assoc : ∀ p1 p2 p3,
  (p1 × (p2 × p3))%pol = ((p1 × p2) × p3) %pol.

Theorem polyn_mul_1_l : ∀ p, (1 × p)%pol = p.

Theorem polyn_mul_add_distr_l : ∀ pa pb pc,
  (pa × (pb + pc))%pol = (pa × pb + pa × pc)%pol.

Theorem polyn_mul_add_distr_r :
  ∀ a b c : polyn T, ((a + b) × c)%pol = (a × c + b × c)%pol.

Theorem polyn_opt_mul_comm :
  if rngl_mul_is_comm T then ∀ a b : polyn T, (a × b)%pol = (b × a)%pol
  else not_applicable.


Theorem polyn_mul_1_r : ∀ a : polyn T, (a × 1)%pol = a.

Theorem polyn_opt_mul_1_r :
  if rngl_mul_is_comm T then not_applicable
  else ∀ a : polyn T, (a × 1)%pol = a.


Theorem polyn_opt_mul_add_distr_r :
   if rngl_mul_is_comm T then not_applicable
   else ∀ a b c : polyn T, ((a + b) × c)%pol = (a × c + b × c)%pol.

Theorem polyn_add_opp_diag_l :
  rngl_has_opp T = true
  → ∀ a : polyn T, (- a + a)%pol = 0%pol.

Theorem polyn_opt_add_opp_diag_l :
  let rop := polyn_ring_like_op in
  if rngl_has_opp (polyn T) then ∀ a : polyn T, (- a + a)%L = 0%L
  else not_applicable.

Theorem polyn_opt_has_no_inv : ∀ P,
  let rop := polyn_ring_like_op in
  if rngl_has_inv (polyn T) then P
  else not_applicable.

Theorem polyn_opt_has_no_inv_and : ∀ e P,
  let rop := polyn_ring_like_op in
  if (rngl_has_inv (polyn T) && e)%bool then P
  else not_applicable.

Notation "a / b" := (polyn_pdiv a b) : polyn_scope.

Theorem polyn_mul_div :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ a b,
  b ≠ 0%pol
  → (a × b / b)%pol = a.

Theorem polyn_opt_mul_div :
  let _ := polyn_ring_like_op in
  if rngl_has_pdiv (polyn T) then ∀ a b, b ≠ 0%L → (a × b / b)%L = a
  else not_applicable.

Theorem lap_polyn_rngl_of_nat_char_0 :
  let _ := polyn_ring_like_op in
  rngl_characteristic T = 0
  → ∀ i, i ≠ 0 → lap (rngl_of_nat i) = [rngl_of_nat i].

Theorem lap_polyn_rngl_of_nat_2 :
  let rop := polyn_ring_like_op in
  ∀ i, 0 < i < rngl_characteristic T
  → lap (rngl_of_nat i) = [rngl_of_nat i].

Let Heo := rngl_has_eq_dec_or_is_ordered_l Hed.

Theorem lap_polyn_rngl_of_nat :
  let lop := lap_ring_like_op Heo in
  let rop := polyn_ring_like_op in
  ∀ n, lap (rngl_of_nat n) = lap_norm (rngl_of_nat n).

Theorem polyn_integral :
  let rop := polyn_ring_like_op in
  ∀ a b : polyn T,
  (a × b)%L = 0%L
  → a = 0%L ∨ b = 0%L ∨ rngl_is_zero_divisor a ∨ rngl_is_zero_divisor b.

Theorem polyn_characteristic_prop : let rop := polyn_ring_like_op in
  if rngl_characteristic T =? 0 then ∀ i : nat, rngl_of_nat (S i) ≠ 0%L
  else
    (∀ i : nat, 0 < i < rngl_characteristic T → rngl_of_nat i ≠ 0%L)
     ∧ rngl_of_nat (rngl_characteristic T) = 0%L.
Theorem rngl_has_opp_rngl_polyn_has_opp :
  let rop := polyn_ring_like_op in
  rngl_has_opp T = rngl_has_opp (polyn T).

Theorem rngl_has_psub_rngl_polyn_has_psub :
  let rop := polyn_ring_like_op in
  rngl_has_psub T = rngl_has_psub (polyn T).

Theorem polyn_opt_add_sub :
  let rop := polyn_ring_like_op in
  if rngl_has_psub (polyn T) then ∀ a b : polyn T, (a + b - b)%L = a
  else not_applicable.


Theorem polyn_opt_sub_add_distr :
  let rop := polyn_ring_like_op in
  if rngl_has_psub (polyn T) then
    ∀ a b c : polyn T, (a - (b + c))%L = (a - b - c)%L
  else not_applicable.

Theorem polyn_opt_sub_0_l :
  let rop := polyn_ring_like_op in
  if rngl_has_psub (polyn T) then ∀ a : polyn T, (0 - a)%L = 0%L
  else not_applicable.

Definition polyn_ring_like_prop : ring_like_prop (polyn T) :=
  {| rngl_mul_is_comm := rngl_mul_is_comm T;
     rngl_is_archimedean := false;
     rngl_is_alg_closed := false;
     rngl_characteristic := rngl_characteristic T;
     rngl_add_comm := polyn_add_comm;
     rngl_add_assoc := polyn_add_assoc;
     rngl_add_0_l := polyn_add_0_l;
     rngl_mul_assoc := polyn_mul_assoc;
     rngl_mul_1_l := polyn_mul_1_l;
     rngl_mul_add_distr_l := polyn_mul_add_distr_l;
     rngl_opt_mul_comm := polyn_opt_mul_comm;
     rngl_opt_mul_1_r := polyn_opt_mul_1_r;
     rngl_opt_mul_add_distr_r := polyn_opt_mul_add_distr_r;
     rngl_opt_add_opp_diag_l := polyn_opt_add_opp_diag_l;
     rngl_opt_add_sub := polyn_opt_add_sub;
     rngl_opt_sub_add_distr := polyn_opt_sub_add_distr;
     rngl_opt_sub_0_l := polyn_opt_sub_0_l;
     rngl_opt_mul_inv_diag_l := polyn_opt_has_no_inv _;
     rngl_opt_mul_inv_diag_r := polyn_opt_has_no_inv_and _ _;
     rngl_opt_mul_div := polyn_opt_mul_div;
     rngl_opt_integral := polyn_integral;
     rngl_opt_alg_closed := NA;
     rngl_opt_characteristic_prop := polyn_characteristic_prop;
     rngl_opt_ord := NA;
     rngl_opt_archimedean := NA |}.

End a.