proposition: Lemma order_cp1 x y: worder x -> worder y -> sub x y -> (sub (substrate x) (substrate y) /\ x = (induced_order y (substrate x))).
proof: Proof. by move => /worder_total wo1 /proj1 wo2 xy; apply: (order_cp1_total). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)