proposition: Lemma order_diff_p2 r1 r2 f (r3 := induced_order r2 ((substrate r2) -s (Imf f))): worder r1 -> worder r2 -> order_morphism f r1 r2 -> segmentp r2 (Imf f) -> worder r3 /\ r2 \Is order_sum2 r1 r3.
proof: Proof. move => ow1 ow2 omf. have ijf:=(order_morphism_fi omf). move:omf => [or1 or2 [ff sf tf] sif segf]. rewrite/r3; set A := (Imf f); set B := substrate r2 -s A. have sbF:sub B (substrate r2) by move => t /setC_P []. have saF:sub A (substrate r2) by exact: (proj1 segf). have ha:= (induced_wor ow2 sbF). split => //. have hb:= (induced_wor ow2 saF). have hbb:= proj1 hb. have haa:= proj1 ha. have res1: r1 \Is (induced_order r2 A). have lax: lf_axiom (Vf f) (source f) A. by move => t ts; apply/(Imf_P ff); ex_tac. exists(Lf (Vf f) (substrate r1) A). split => //. rewrite iorder_sr//; saw; rewrite - sf;apply:lf_bijective. - done. - move => u v usf vsf sv; exact: (proj2 ijf _ _ usf vsf sv). - by move => y /(Imf_P ff). hnf; aw;rewrite - sf;move => x y xE yE; rewrite !LfV//. apply:(iff_trans (sif x y xE yE)) . apply:iff_sym; exact:(iorder_gle0P r2 (lax _ xE) (lax _ yE)). apply:(orderIT (order_diff_p1 (worder_total ow2) segf)). apply (orsum_invariant4 (orderIS res1) (orderIR haa)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)