proposition: Lemma total_order_counterexample (r := (subp_order C2)): lattice r /\ ~ (total_order r).
proof: Proof. split; [ apply:setP_lattice | move=> [or]]. rewrite (proj2 (subp_osr C2)) => to. have sa: (inc (singleton C0) (\Po C2)). apply/setP_P; move=> t /set1_P ->; fprops. have sb: (inc (singleton C1) (\Po C2)). apply/setP_P; move=> t /set1_P ->; fprops. case: (to _ _ sa sb) => /subp_gleP [_ _] /sub1setP /set1_P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)