proposition: Lemma nf_rev_sum 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 (v==zero) then (w = u /\ p = (n + m)%N) else (w = u+v /\ p = m).
proof: Proof. move => nu nv. move: (nf_rev nu)(nf_rev nv); rewrite -/u -/v -/n -/m; move => [sa sb][sc sd]. case pa: (v==zero). have eq3: x + y = T1omega *u + \F (n + m). by rewrite sb sd (eqP pa) T1muln0 T1add0n - T1addA add_int. by move: (nf_rev_unique (n+m)%N sa); rewrite - eq3; move => [-> ->]. have eq3: x +y = T1omega * (u + v) + \F m. by rewrite sb sd -T1addA (T1addA (\F n)) plus_int_Ox ?pa // T1addA mul_distr. by move: (nf_rev_unique m (nf_add sa sc)); rewrite - eq3; move => [-> ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)