proposition: Lemma total_subordersP r x: inc x (total_suborders r) <-> (sub x (substrate r) /\ total_order (induced_order r x)).
proof: Proof. split; first by move=> /Zo_P[/setP_P ha hb]. by move => [ha hb]; apply/Zo_P; split => //; apply /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)