proposition: Lemma odivision_exists_alt a b c: ordinalp a -> ordinalp b -> ordinalp c -> a <o (b *o c) -> exists q r, odiv_pr1 a b c q r.
proof: Proof. move=> oa ob oc [] /ordinal_le_P0; rewrite /oprod2. set pbc:= (order_prod2 _ _) => qa qb. move: (conj qa qb) => a_bc; clear qa qb. have obc: worder pbc by rewrite /pbc; fprops. move: (ordinal_lt_pr2 obc a_bc) => [f [x [xsp rgx om]]]. have orb: order (ordinal_o b) by fprops. have orc: order (ordinal_o c) by fprops. have ora: order (ordinal_o a) by fprops. move: (ordinal_o_sr b) (ordinal_o_sr c) => sb sc. move: (xsp); rewrite orprod2_sr // setX2_P. rewrite sb sc;move=> [fgx dx xa xb]. have [w wsb wle]: exists2 w, inc w b & (forall t, inc t b -> gle (ordinal_o b) w t). have nesb: nonempty (substrate (ordinal_o b)) by rewrite sb;ex_tac. move: (worder_least (ordinal_o_wor ob) nesb)=> [w [p1 p2]]. rewrite sb in p1 p2; ex_tac. set y := variantLc (Vg x C0) w. have ysp: inc y (substrate pbc). rewrite orprod2_sr //; apply /setX2_P; rewrite sb sc /y; aw; split;fprops. set r := (Vg x C1) ; set q := (Vg x C0). have lt_rb: r <o b by apply /oltP0; split => //; exact (Os_ordinal ob xb). have lt_qc: q <o c by apply /oltP0; split => //; exact (Os_ordinal oc xa). have oq:= proj31_1 lt_qc. have odr:= proj31_1 lt_rb. have worr: worder (ordinal_o r) by fprops. have orq: order (ordinal_o q) by fprops. have sq :=(ordinal_o_sr q). have sqc: sub q c by move: lt_qc => [[_ _ h] _]. have srb: sub r b by move: lt_rb => [[_ _ h] _]. exists q, r; split => //; split => //. have rsub: forall r A u v, order r -> sub A (substrate r) -> (gle (induced_order r A) u v <-> [/\ inc u A, inc v A & gle r u v]). move=> r0 A0 u v or Asr; split. move /setI2_P => [pa] /setXp_P [ua va];split => //. by move=> [uA vA rr]; apply /iorder_gleP. set A:= segment pbc y. have iuA: A = product2 q b. have pa: inc C0 (doubleton C0 C1) by fprops. have pb: inc C1 (doubleton C0 C1) by fprops. set_extens u. move /segmentP => [] /(orprod2_gleP orb orc). rewrite sb sc variant_V_ca variant_V_cb. move=> [pc v2p h] unv. move: pc => /setX2_P [fgu du ua ub]; apply /setX2_P => //. case: h;last by move /(ordo_ltP oc ua xa). move=> [r1 r2]; move: (wle _ ub) => r3. have Wv: w = (Vg u C1) by order_tac. case: unv;rewrite /y;apply: fgraph_exten => //; [fprops | by aw |]. rewrite du; move=> x0 x0d; try_lvariant x0d; ue. move /setX2_P => [fgu du ua ub]. have uc:inc (Vg u C0) c by apply: sqc. apply /segmentP; split; last first. move => uy; case: (ordinal_irreflexive oq). move: ua; rewrite uy /y variant_V_ca //. apply /(orprod2_gleP orb orc); rewrite sb sc;split => //. + by apply /setX2_P. + rewrite /y;apply /setX2_P;aw;split;fprops. + right; rewrite variant_V_ca; apply /(ordo_ltP oc uc) => //. have ss3: substrate pbc = product2 c b by rewrite orprod2_sr // sb sc. have ss2: sub A (substrate pbc) by apply: sub_segment. have sA: sub A (product2 c b) by ue. have wo2: worder (induced_order pbc A) by apply: induced_wor. have obq: ordinalp (b *o q) by fprops. have ->:b *o q = ordinal (induced_order pbc A). symmetry; apply: ordinal_o_isu2 => //. set r1 := (order_prod2 (ordinal_o b) (ordinal_o q)). have wo1: worder r1 by rewrite /r1; fprops. apply: orderIT (ordinal_o_is wo1). have or2:order (induced_order pbc A) by fprops. have or1:order r1 by fprops. suff: r1 = (induced_order pbc A) by move=> ->; apply: orderIR. apply: order_exten => // u v; split. move /(orprod2_gleP orb orq);rewrite sb sq; move => [pa pb pc]. apply /iorder_gle0P; try ue; apply /(orprod2_gleP orb orc). rewrite sb sc; split => //; try( apply :sA ; ue). case: pc; [ by left | move => [ /ordo_leP [sa ssb ssc] sd] ; right ]. split => //;apply /ordo_leP;split;fprops. move => /iorder_gleP [uA vA] /(orprod2_gleP orb orc) [_ _ h]. apply /(orprod2_gleP orb orq); rewrite sb sq;split => //; try ue. case: h; [by left | move=> [/ordo_leP [sa ssb ssc] sd]; right]. move: uA vA;rewrite iuA;move /setX2_P => [_ _ uq _] /setX2_P [_ _ vq _]. split => //;apply /ordo_leP;split;fprops. set C := induced_order pbc (segment pbc x). have oraC: C \Is (ordinal_o a). have injf:= (order_morphism_fi om). move: om=> [o1 o2 [ff sf tf] mof]. apply: orderIS; rewrite /C -rgx. have sr: sub (Imf f) (substrate pbc). rewrite - tf; fprops; apply: Imf_Starget =>//. have o3:= (proj1(iorder_osr o2 sr)). have aux: (source (restriction1 f (source f))) = source f. by rewrite /restriction1; aw. exists (restriction1 f (source f)); split => //. hnf; rewrite{2 3}/restriction1 iorder_sr //; saw. by apply:(restriction1_fb injf). red; rewrite aux => u v usf vsf;rewrite restriction1_V // restriction1_V //. rewrite /pbc mof // rsub //; split; last by move => [_ _]. move=> Wuv; split => //; Wtac. rewrite - (ordinal_o_o oa) -(ordinal_o_o odr). have opbc: order pbc by fprops. symmetry;apply: orsum_invariant5 => //. apply: orderIT oraC. set fo:= order_sum2 _ _. have sfo: substrate fo = canonical_du2 A r. by rewrite /fo orsum2_sr//? iorder_sr //; fprops; rewrite ordinal_o_sr. have ysp': inc y (product2 c b) by ue. have xsp': inc x (product2 c b) by ue. have lexy: gle pbc y x. apply /(orprod2_gleP orb orc); rewrite sb sc /y;aw; split => //; left. by split => //;apply: wle. have ltAx: forall t, inc t A -> glt pbc t x. move =>t /segmentP lttxy; order_tac. have rprop: forall z, inc z r -> inc (variantLc (Vg x C0) z) (product2 c b). move=> z zB; apply /setX2_P; aw; split;fprops. have p1: forall z, inc z r -> gle pbc y (variantLc (Vg x C0) z). move=> z zB; apply /(orprod2_gleP orb orc); rewrite sb sc; split;fprops. by rewrite /y;aw;left; split => //; apply: wle; apply: srb. set g := fun z => Yo (Q z = C0) (P z) (variantLc (Vg x C0) (P z)). have ssx: sub (segment pbc x) (substrate pbc) by apply: sub_segment. have srC: substrate C = (segment pbc x) by rewrite /C iorder_sr. have ta: forall z, inc z (substrate fo) -> inc (g z) (substrate C). move=> z; rewrite sfo; move /candu2P=> [pz xx]. rewrite srC; apply /segmentP;case :xx. by move => [Pz Qz]; rewrite /g; Ytac0;apply: ltAx => //. move => [Pz Qz]; rewrite /g Qz; Ytac0; split; last first. by move => bad; case: (ordinal_irreflexive odr); rewrite {1} /r -bad; aw. apply /(orprod2_gleP orb orc); rewrite sb sc. move /(ordo_ltP ob (srb _ Pz) xb): (Pz) => [pa pb]. split; [ by apply: rprop | exact | left]. by rewrite variant_V_ca variant_V_cb. have bg: bijection (Lf g (substrate fo) (substrate C)). apply: lf_bijective => //. move=> u v; rewrite sfo /g; move /candu2P => [pu p3] /candu2P [pv p4]. case: p3; case: p4; move=> [p5 p6][p7 p8];rewrite p6 p8; Ytac0; Ytac0=> aux. + by apply: pair_exten =>//; ue. + move/segmentP: p7 => lt1;move:(p1 _ p5);rewrite -aux => lt2; order_tac. + move/segmentP:p5 => lt1; move:(p1 _ p7); rewrite aux => lt2; order_tac. + by apply: pair_exten => //; [ move: (f_equal (Vg ^~ C1) aux); aw | ue ]. move=> v; rewrite srC => /segmentP hyp. case: (p_or_not_p (glt pbc v y)) => aux. exists (J v C0); last by rewrite /g; aw; Ytac0. rewrite sfo; apply /candu2P; split;fprops;left. by saw; apply /segmentP. move: hyp aux => [] /(orprod2_gleP orb orc); rewrite sb sc. move => [vp xp aux] nvx cvy. case: aux; last first. move=> aux2; case: cvy. split; last by rewrite /y;move: aux2 =>[_ vx]; dneg ww; rewrite ww; aw. apply /(orprod2_gleP orb orc); rewrite sb sc. by split => //;rewrite /y; aw; right. move=> [sva leva]. have vpr: v = variantLc (Vg x C0) (Vg v C1). move: vp => /setX2_P [a1 a2 a3 a4]. apply: fgraph_exten => //;[ fprops | by aw |]. by rewrite a2; move => z zd; try_lvariant zd. have ltva:glt (ordinal_o b) (Vg v C1) (Vg x C1). split => //; clear cvy; dneg ww; rewrite vpr ww. symmetry; move:xp => /setX2_P [a1 a2 _ _]. apply: fgraph_exten => //;[ fprops | by aw |]. by rewrite a2; move => z zd; try_lvariant zd. exists (J (Vg v C1) C1); last by rewrite /g; aw; rewrite -vpr; Ytac0. rewrite sfo;apply: candu2_prb => //. move /ordo_leP: leva => [pa pb pc]. by apply /(ordo_ltP ob pa pb). exists (Lf g (substrate fo) (substrate C)). apply: total_order_isomorphism; rewrite ? lf_source ? lf_target //. rewrite /fo;apply: orsum2_totalorder => //. apply: total_order_sub => //;apply: worder_total => //. apply: worder_total => //. apply: (proj1 (iorder_osr opbc ssx)). rewrite sfo; rewrite sfo in ta. have oiA: order (induced_order pbc A) by fprops. have oor: order (ordinal_o r) by fprops. move=> u v uc vc /=; rewrite LfV // LfV // /fo /C rsub //. move /orsum2_gleP => [_ _ h]; rewrite - srC;split => //; try (apply: ta => //). rewrite /g; case: h. move=> [h1 h2 h3]; Ytac0; Ytac0; apply: (iorder_gle1 h3). move=> [h1 h2 h3]; Ytac0; Ytac0. apply /(orprod2_gleP orb orc); rewrite sb sc; aw. move /ordo_leP: h3 => [h3 h4 h5]. split; [by apply: rprop | by apply: rprop | left; split => //]. by apply /ordo_leP; split => //; apply: srb. move => [h1 h2]; Ytac0; Ytac0. move/candu2P: uc => [_]; case; last by move => [_ bad]; case: C1_ne_C0; ue. move => [/segmentP [pa _] _]. move/candu2P: vc => [_];case; [ by move=> [_] | move=> [/p1 h0 _]; order_tac]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)