proposition: Lemma lt_succ_succ x y: T2succ x < T2succ y -> x < y.
proof: Proof. elim: x y; first by case; [ rewrite T2ltnn | move => a b n c _ ]. move => a _ b _ n c Hc /=; case. rewrite {2}/T2succ T2lt1; case: ([a, b] == one) => //. move => a' b' n' c'; case sa: ([a, b] == one) => /=. case /eqP:sa => -> -> /=;case sb: ([a', b'] == one) => //. rewrite {1} /T2lt /= if_same if_simpl ltnS. by case /eqP:sb => -> ->; rewrite /T2lt /= => ->. move => _; rewrite T2lt_consE /lt_psi !T2ltn0 !T2lt0n /=. move: sb; rewrite T2eqE !eqxx !(eq_sym zero) !andbT. by case az: (a' == zero) => //= ->. case pa: ([a', b'] == one); rewrite !T2lt_consE. by rewrite -T2lt_psi T2lt1 /=; move: sa; rewrite T2eqE !andbT => ->. case: (lt_psi a b a' b') => //; case:((a == a') && (b == b')) => //. case: (ltngtP n n') => // _;apply: Hc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)