proposition: Lemma order_diff_p1 A r (r1 := induced_order r A) (r2 := induced_order r ((substrate r) -s A)): total_order r -> segmentp r A -> r \Is order_sum2 r1 r2.
proof: Proof. move => [or tor] segf. set B := substrate r -s A. have sbF:sub B (substrate r) by move => t /setC_P []. have saF:sub A (substrate r) by exact: (proj1 segf). move: (iorder_osr or saF) => [orA srA]. move: (iorder_osr or sbF) => [orB srB]. apply:orderIS. case:(orsum2_osr orA orB). set r5 := order_sum2 _ _ => or5 sr5'. move:(sr5'); rewrite ! iorder_sr //; move => sr5. have ax: forall x, inc x (substrate r5) -> inc (P x) (substrate r). rewrite sr5 => x /candu2P [_]; case => [] [pp _]; fprops. exists (Lf P (substrate r5) (substrate r)); split => //. saw; apply: lf_bijective. - exact. - rewrite sr5;move => x y /candu2P [px pxx] /candu2P [py pyy] sp. apply: (pair_exten px py sp). case: pxx => [][qa ->]; case: pyy => [][qb ->] //. by case/setC_P: qb => _; rewrite - sp. by case/setC_P: qa => _; rewrite sp. - rewrite sr5;move => y ysr2; case: (inc_or_not y A) => yA. by exists (J y C0); aw;trivial; apply: candu2_pra. by exists (J y C1); aw; trivial;apply: candu2_prb; apply:setC_i. hnf; aw; move => x y xs ys; rewrite !LfV//. move:(xs); rewrite sr5 => /candu2P [xa xb]. move:(ys); rewrite sr5 => /candu2P [ya yb]. move:(orsum2_gleP (induced_order r A) (induced_order r B) x y). rewrite - sr5' -/r5 => H; split. move: C1_ne_C0 => ba; move:(nesym ba) => bb. move/H => [_ _]; case. + by move => [_ _]; case/iorder_gleP. + by move => [_ _]; case/iorder_gleP. + move => [qx qy]; case: xb; last by rewrite qx;move => [_] //. case: yb => [] [pyb] // _ [pxa _]. have pxr: inc (P x) (substrate r) by apply: saF. have pyr: inc (P y) (substrate r) by apply: sbF. case: (tor (P x) (P y) pxr pyr) => // lpp. case/setC_P: pyb =>_ []; exact:(proj2 segf (P x) (P y) pxa lpp). move => lexy; apply/H; split => //. case: yb => [] [yA ->]. move: (proj2 segf (P y) (P x) yA lexy) => xA. constructor 1; split. + by case: xb => [][] //;case/setC_P. + done. + by apply/iorder_gleP. case: xb => [] [xA ->]; first by constructor 3; split => //; fprops. by constructor 2; split => //; fprops;apply/iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)