proposition: Lemma torder_set1 r x: order r -> inc x (substrate r) -> inc (singleton x) (total_suborders r).
proof: Proof. move => or xsr. have h: sub (singleton x) (substrate r) by move => t /set1_P ->. apply: (total_suborder_prop or h) => a b /set1_P-> /set1_P ->; left. by order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)