proposition: Lemma nf_rev_unique u v (x:= T1omega *u + \F v): T1nf u -> u = T1div_by_omega (T1split x).1 /\ v = (T1split x).2.
proof: Proof. suff H: forall u v u' v', T1nf u -> T1nf u' -> T1omega * u + \F v = T1omega * u' + \F v' -> u = u' /\ v = v'. move => nu. have nx: T1nf x by rewrite nf_add // ? nf_finite // nf_mul. move: (nf_rev nx) => []; by apply: H. clear x u v. move => u v u' v' nu nu' h. have aux1: forall a b, T1omega * a + \F b < T1omega * (T1succ a). by move => a b; rewrite mul_succ // T1lt_add2l; case b. have aux2: forall a b, T1omega * a <= T1omega * a + \F b. move => a b; apply: add_le1. move: (aux1 u v) (aux2 u' v'); rewrite h => sa sb. move: (T1le_lt_trans sb sa); rewrite T1lt_mul2l // ?nf_succ // lt_succ_le_3 //. move: (aux1 u' v') (aux2 u v); rewrite h => ta tb. move: (T1le_lt_trans tb ta); rewrite T1lt_mul2l // ?nf_succ // lt_succ_le_3 //. move => sc sd. have uu': u = u' by move: sc sd; rewrite /T1le (eq_sym u'); case (T1ltgtP u u'). by move: h; rewrite uu' => /eqP; rewrite T1eq_add2l => /T1eqP /T1F_inj ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)