proposition: Lemma odivision_exists a b c: ordinalp b -> ordinalp c -> a <o (b *o c) -> odiv_pr1 a b c (oquo a b) (orem a b).
proof: Proof. move => ob oc lac. have oa := (proj31_1 lac). have osa := (OS_succ oa). case: (ozero_dichot ob) => bp; first by move: lac; rewrite bp oprod0l => /olt0. pose p z := a = b *o (P z) +o (Q z). move /(oltP (OS_prod2 ob oc)):lac; rewrite (oprod_rec_def ob oc). move => /funI_P [z /setX_P [za /(oltP ob) zb /(oltP oc) zc] eqa]. set E := (osucc a) \times b. have pz: p (J (Q z) (P z)) by rewrite/p; aw. move:(proj31_1 zb)(proj31_1 zc)=> or oq. have ze: inc (J (Q z) (P z)) E. apply: setXp_i; [apply/(oleP oa) | by apply/(oltP ob) ]. move: (osum_Mle0 (OS_prod2 ob oq) or); rewrite - eqa; apply: oleT. apply:(oprod_M1le bp oq). have pb:singl_val2 (inc^~ E) p. move => u v /setX_P [pu /(oltP osa) oq'' /(oltP ob) or''] vu. move => /setX_P [pv /(oltP osa) oq' /(oltP ob) or'] vv. move: (proj31_1 or'')(proj31_1 oq'') => r1 r2. move: (proj31_1 or')(proj31_1 oq') => r1' r2'. have ha: odiv_pr0 a b (P u) (Q u) by []. have hb: odiv_pr0 a b (P v) (Q v) by []. by move: (odivision_unique oa ob ha hb) => [hc hd]; apply/pair_exten. move: (select_uniq pb ze pz) => eqb. by rewrite /odiv_pr1 /oquo/orem -[oquorem a b] eqb; saw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)