proposition: Lemma total_order_directed r: total_order r -> (right_directed r /\ left_directed r).
proof: Proof. by move=>to; apply: lattice_directed; apply: total_order_lattice. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)