proposition: Lemma lt_succ_succ x y: T3succ x < T3succ y -> x < y.
proof: Proof. elim: x y; first by case; [ rewrite T3ltnn | move => a b c n d _ ]. move => a _ b _ c _ n d Hd /=; case. by rewrite {2}/T3succ T3lt1; case (all_zero a b c) => //. move => a' b' c' n' d'; rewrite all_zeroE;case sa: ([a, b, c] == one). rewrite /= all_zeroE; case sb: ([a', b', c'] == one). rewrite {1} /T3lt /= if_same if_simpl ltnS T3lt_consE (eqP sb) sa => ->. by rewrite if_same. by move => _; rewrite T3lt_consE (eqP sa) T3gt1 sb. rewrite /= all_zeroE;case: eqP => /=. by move => sb; rewrite T3lt_consE T3lt1 /= sa. move => _; rewrite T3lt_consE => h; rewrite T3lt_consE; move: h. case: (T3ltgtP [a, b, c] [a', b', c']) => // _. case (ltngtP n n') => // _; apply: Hd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)