proposition: Lemma total_order_lattice r: total_order r -> lattice r.
proof: Proof. move=> [or tor]; split=>//. move=> x y xsr ysr; case: (tor _ _ xsr ysr). move => hyp; split. by exists y; apply: sup_comparable. by exists x; apply: inf_comparable. rewrite set2_C => hyp; split. by exists x; apply: sup_comparable. by exists y; apply: inf_comparable. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)