proposition: Lemma T3lt_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; [ by case | move => a b c n d;case => // => a' b' c' n' d']. set l:= (size (cons a b c n d) + size (cons a' b' c' n' d'))%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 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 T3lt_consE T3lt_psi T3lt_consE T3lt_psi !T3eqE /lt_psi. case /or3P:(Hr _ _ pa) => caa'; last 1 first. + rewrite caa' (T3lt_anti caa') (T3lt_ne caa') (T3lt_ne' caa') !orbF !if_simpl. rewrite /= (eq_sym _ c) (eq_sym _ b). case /or3P: (Hr _ _ pj) => ->; rewrite ?orbT //=. by case /or3P: (Hr _ _ ph) => -> //=; rewrite ?orbT. + rewrite caa' (T3lt_anti caa') (T3lt_ne caa')(T3lt_ne' caa') !orbF !if_simpl. case /or3P: (Hr _ _ pg) => ->; rewrite ?orbT //=. case /or3P: (Hr _ _ pi) => ->; rewrite ?orbT //=. + rewrite caa' (eqP caa') T3ltnn eqxx /= !orbF. case /or3P:(Hr _ _ pb) => cbb'; last 1 first. * rewrite cbb' (T3lt_anti cbb') (T3lt_ne' cbb'). simpl. by case /or3P: (Hr _ _ pi) => h; rewrite h /= ? orbT. * rewrite cbb' (T3lt_anti cbb') (T3lt_ne cbb') (T3lt_ne' cbb') (eq_sym _ c). by rewrite -(eqP caa'); case /or3P:(Hr _ _ pj) => h; rewrite h ?orbT. * rewrite (eqP cbb') T3ltnn !eqxx /=. case /or3P: (Hr _ _ pc) => h; rewrite h // ?orbT //(eqP h) T3ltnn eqxx /=. case (ltngtP n n') => // _; rewrite Hr //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)