proposition: Lemma diagonal_length_contra r: order r -> order_length r \1c -> r = diagonal (substrate r).
proof: Proof. move => or [qa qb]. set_extens t; last by move/diagonal_i_P => [{4} <- ps <-]; order_tac. move => tr; apply /diagonal_i_P. move: (proj41 or _ tr) (pr1_sr tr) (pr2_sr tr) => pt Ps Qs. have qc:sub (doubleton (P t) (Q t)) (substrate r) by apply: sub_set2. split => //; ex_middle bad. have: inc (doubleton (P t) (Q t)) (total_suborders r). apply:(total_suborder_prop or qc) => a b. case/set2_P => ->;case/set2_P => ->. + by left; order_tac. + by left; rewrite /gle/related pt. + by right; rewrite /gle/related pt. + by left; order_tac. move/qb; rewrite(cardinal_set2 bad) => /cleNgt; case; exact: clt_12. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)