proposition: Lemma T2lt_anti b a: a < b -> (b < a) = false.
proof: Proof. set n := (size a + size b).+1. move: (leqnn n); rewrite {1}/n; move: n => n. elim: n a b; first by move => a b //;rewrite ltn0. move => m Hrec a b; rewrite ltnS. case: a b => [ [] // | a b n c [] // a' b' n' c']. set l:= (size (cons a b n c) + size (cons a' b' n' c'))%N => lm. have Hr : forall a b, (size a + size b < l)%N -> a < b -> (b < a) = false. by move => u v ll; apply: Hrec; apply: (leq_trans ll lm). move: (size_prop a b n c a' b' n' c'); rewrite -/l. move => [pa [pb [pc [pd [pe pf]]]]]. rewrite !T2lt_consE /lt_psi. case qa: (a < a'). rewrite (Hr a a' pf qa) (T2lt_ne qa) (T2lt_ne' qa) !andFb /= !orbF !if_simpl. by move => qc;rewrite (T2lt_ne' qc) (Hr _ _ pe qc). case qa': (a' < a). rewrite (T2lt_ne qa') (T2lt_ne' qa') /= !orbF !if_simpl; case /orP. exact/(Hr _ _ pb). by move /eqP ->; rewrite T2ltnn. rewrite /= !orbF (eq_sym a' a) (eq_sym b' b) (eq_sym n' n). case: eqP => //= _. case qb: (b < b'); first by rewrite (Hr b b' pd qb) (T2lt_ne qb). case qb': (b' < b); first by rewrite (T2lt_ne' qb'). by case: eqP => //= _;case: (ltngtP n n') => // _; apply: Hr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)