proposition: Lemma T3lt_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. 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 -> (b < a) = false. 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 qa: (a < a'). rewrite (Hr a a' pe qa) (T3lt_ne qa) (T3lt_ne' qa) !andFb /= !orbF if_simpl. move => /andP [qc qd]; rewrite (T3lt_ne' qc) (T3lt_ne' qd). by rewrite (Hr _ _ ph qc) (Hr _ _ pj qd). case qa': (a' < a). rewrite (T3lt_ne qa') (T3lt_ne' qa') /= !orbF !if_simpl; case /or4P. + by move /(Hr _ _ pg) ->. + by move /eqP ->; rewrite T3ltnn. + by move /(Hr _ _ pi) ->; rewrite andbF. + by move /eqP ->; rewrite T3ltnn andbF. rewrite /= (eq_sym a' a) (eq_sym b' b) (eq_sym c' c) (eq_sym n' n). case aa: (a== a') => //=. case qb: (b < b'). rewrite (T3lt_ne qb) (Hr _ _ pb qb) /= !orbF !if_simpl => h. by rewrite (Hr _ _ pj h) (T3lt_ne' h). case qb': (b' < b). rewrite (T3lt_ne' qb') /= orbF !if_simpl. by case /orP => h; [rewrite (Hr _ _ pi h) | rewrite (eqP h) T3ltnn ]. case bb: (b== b') => //=. case qc: (c < c'); first by rewrite (Hr c c' pc qc) (T3lt_ne qc). case qc': (c' < c); first by rewrite (T3lt_ne' qc'). by case cc: (c== c') => //=;case: (ltngtP n n') => // _; apply: Hr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)