proposition: Lemma T2lt_trichotomy a b: [|| (a< b), (a==b) | (b < a)].
proof: Proof. set n := (size a + size b).+1. move: (leqnn n); rewrite {1}/n; move: n. move => 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), (a==b) | (b < a)] 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 /or3P:(Hr _ _ pf) => caa'; last 1 first. + rewrite caa' (T2lt_anti caa') (T2lt_ne caa') (T2lt_ne' caa') !orbF !if_simpl. by case /or3P: (Hr _ _ pb) => -> //; rewrite !orbT //. + rewrite caa' (T2lt_anti caa') (T2lt_ne caa')(T2lt_ne' caa') !orbF !if_simpl. by rewrite /= (eq_sym _ b); case /or3P: (Hr _ _ pe) => -> //; rewrite !orbT. + rewrite caa' (eqP caa') T2ltnn eqxx /= !orbF. case /or3P:(Hr _ _ pd) => cbb'; last 1 first. * by rewrite cbb' (T2lt_anti cbb') (T2lt_ne' cbb') ! orbT. * by rewrite cbb'. * rewrite (eqP cbb') T2ltnn eqxx; case: (ltngtP n n') => //; rewrite ?orbT //. move => ->; case /or3P:(Hr _ _ pa) => cc; rewrite ? cc ?orbT //. by rewrite (eqP cc) eqxx orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)