proposition: Lemma total_suborder_prop r X: order r -> sub X (substrate r) -> {inc X &, forall x y, ocomparable r x y} -> inc X (total_suborders r).
proof: Proof. move => or Xsr ac. move: (iorder_osr or Xsr) => [or1 sr1]. apply/total_subordersP; split => //; split => //; rewrite sr1 => x y xA yA. by case: (ac _ _ xA yA) => cp; [left | right]; apply/iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)