proposition: Lemma lt_succ_le_2 a b: T2nf a -> a < T2succ b -> a <= b.
proof: Proof. elim: a b; first by move => b;rewrite T2le0n. move => a' _ b' _ n' c' Hc; case; first by rewrite T2lt1 => _ /eqP ->. move => a b n c nx /=; case sa: ([a, b] == one). case /eqP: sa => -> ->; rewrite T2lt_consE T2le_consE -T2lt_psi T2lt1 /=. case sa: ((a' == zero) && (b' == zero)) => //. have sa': ([a',b']==one) by rewrite T2eqE !andbT sa. rewrite (T2nf_finite sa' nx) ltnS leq_eqVlt if_same T2le0n. by case (ltngtP n' n). rewrite T2lt_consE T2le_consE; case: (lt_psi _ _ _ _) => //. case: (_ && _) => //; case: (ltngtP n' n) => // _. by apply: Hc; move:nx => /and4P[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)