proposition: Lemma tor_prop r: {inc substrate r &, forall x y , ocomparable r x y} -> forall x y, inc x (substrate r) -> inc y (substrate r) -> gle r x y \/ glt r y x.
proof: Proof. move=> tor x y xs ys; case: (tor _ _ xs ys); first by left. move=> aux; case:(equal_or_not x y) => h; first by left; move: aux;rewrite h. by right; split => //; apply:nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)