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