proposition: Lemma total_order_dlattice r: total_order r -> distributive_lattice1 r.
proof: Proof. move=> [or tor] a b c ar br cr. case: (tor _ _ ar br) => ab. rewrite (sup_comparable1 or ab); case: (tor _ _ ar cr) => ac. rewrite (sup_comparable1 or ac); case: (tor _ _ br cr) => bc. by rewrite (inf_comparable1 or bc) (sup_comparable1 or ab). by rewrite(inf_C r b c) (inf_comparable1 or bc)(sup_comparable1 or ac). rewrite (sup_C r a c)(sup_comparable1 or ac). rewrite (inf_C r b a) (inf_comparable1 or ab). have cb: (gle r c b) by order_tac. rewrite (inf_C r b c) (inf_comparable1 or cb). by rewrite (sup_C r a c) (sup_comparable1 or ac). rewrite (sup_C r a b) (sup_comparable1 or ab). case: (tor _ _ ar cr) => ac. rewrite (sup_comparable1 or ac) (inf_comparable1 or ac). have bc: (gle r b c) by order_tac. by rewrite (inf_comparable1 or bc) (sup_C r a b) (sup_comparable1 or ab). rewrite (sup_C r a c) (sup_comparable1 or ac). have aa: (gle r a a) by order_tac. rewrite (inf_comparable1 or aa). case: (tor _ _ br cr) => bc. by rewrite (inf_comparable1 or bc) (sup_C r a b) (sup_comparable1 or ab). rewrite (inf_C r b c) (inf_comparable1 or bc). by rewrite (sup_C r a c) (sup_comparable1 or ac). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)