proposition: Lemma nf_rev_prod x y (u := T1div_by_omega (T1split x).1) (n:= (T1split x).2) (v := T1div_by_omega (T1split y).1) (m:= (T1split y).2) (w := T1div_by_omega (T1split (x*y)).1) (p:= (T1split (x*y)).2): T1nf x -> T1nf y -> if (u== zero) then if (n == 0) then (w = zero /\ p = 0) else (w = v /\ p = (n*m)%N) else if (m==0) then (w = u * T1omega *v /\ p = 0) else (w = u * T1omega *v + u * \F m /\ p = n).
proof: Proof. move => nu nv. set H := nf_rev_unique. move: (nf_rev nu)(nf_rev nv); rewrite -/u -/v -/n -/m; move => [sa sb][sc sd]. case pa: (u== zero). have : x * y = (\F n) * T1omega * v + \F (n * m)%N. by rewrite sb sd (eqP pa) T1muln0 T1add0n mul_distr mul_int mulA. case n; first by rewrite /w /p /= T1mul0n T1add0n => ->. move => n'; rewrite mul_fin_omega /= => h. by move: h (H _ (n'.+1 * m)%N sc) => <- [-> ->]. move: (erefl (x* y)); rewrite {2} sd mul_distr mulA. rewrite {2} sb mul_sum_omega ? pa // - !mulA => h. have se: T1nf (u * (T1omega * v)) by rewrite !nf_mul //. have sf: T1nf (u * (T1omega * v) + u * \F m). by rewrite nf_add // nf_mul // nf_finite. have aux: T1nf (T1omega * u) by rewrite nf_mul. case pb: (m==0). by move: h (H _ 0 se); rewrite (eqP pb) T1muln0; move => <- [-> ->]. have e1: \F n + x = x by rewrite sb T1addA plus_int_Ox ? pa //. have e2: x * \F m = T1omega * u * \F m + \F n. move: pb;elim m => // k Hr _; case ba: (k== 0). by rewrite (eqP ba) T1muln1 // T1muln1. rewrite - (addn1) - add_int mul_distr Hr // T1muln1 // - T1addA e1 sb. by rewrite T1addA mul_distr T1muln1. by move: h (H _ n sf); rewrite e2 T1addA - mulA - mul_distr => <- [-> ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)