proposition: Lemma T2ltE x y : x < y = lt_rec T2lt x y.
proof: Proof. have aux: forall n x y, ((size x + size y) < n)%N -> T2lta n x y = (x < y). clear x y;move => n; elim: n {1 3 4} n (leqnn n); first by case. move => k0 Hrec; case => // k1; rewrite ltnS => k1k0. case => // a b n c; case => // a' b' n' c'. rewrite /T2lt; set l := addn _ _; rewrite ltnS => e3. move: (leq_trans e3 k1k0) => e4. move: (size_prop a b n c a' b' n' c'). rewrite -/l;move => [pa [pb [pc [pd [pe pf]]]]]. rewrite /T2lta /lt_rec -/lt_rec -/T2lta. by rewrite ! Hrec //; apply:(leq_trans _ e3). case x => // a b n c; case:y => // a' b' n' c'. move: (size_prop a b n c a' b' n' c') => [pa [pb [pc [pd [pe pf]]]]]. by rewrite /lt_rec {1} /T2lt /T2lta -/T2lta {1} /lt_rec -/lt_rec !aux. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)