proposition: Lemma order_cp1_total x y: total_order x -> order y -> sub x y -> (sub (substrate x) (substrate y) /\ x = (induced_order y (substrate x))).
proof: Proof. move => to1 o2 xy. move: (proj1 to1) => o1. have aa: sub (substrate x) (substrate y). move => t tsa; apply /(order_reflexivityP o2); apply: xy. by apply /(order_reflexivityP o1). have [sa sb]:=(iorder_osr o2 aa). split => //; apply: extensionality. move => t tx; apply /setI2_P; split; fprops. apply:sub_graph_coarse_substrate; fprops. move => t /setI2_P [ty /setX_P [pa pb pc]]; rewrite - pa. case: (proj2 to1 _ _ pb pc) => // h2. rewrite -pa in ty. move: (order_antisymmetry o2 (xy _ h2) ty) => h3; by move: h2; rewrite h3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)