proposition: Lemma total_order_width_contra r: order r -> order_width r \1c -> total_order r.
proof: Proof. move => or [ha hb]. split => // u v usr vsr; ex_middle bad. have hc: inc (doubleton u v) (free_subsets r). apply/free_subsetsP; split; first by apply:sub_set2. move => a b /set2_P; case => ->; case/ set2_P => -> // h; case: bad. by left. by right. case: (equal_or_not u v) => neq. by case: bad; left; rewrite neq; order_tac. move: (hb _ hc); rewrite (cardinal_set2 neq) => /cleNgt; case; exact: clt_12. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)