proposition: Lemma oquoremP a b: ordinalp a -> \0o <o b -> odiv_pr0 a b (oquo a b) (orem a b).
proof: Proof. move => oa bp. have osa := (OS_succ oa). have ob := (proj32_1 bp). have la: a <o (b *o (osucc a)) by apply /oleSltP; apply:oprod_M1le. exact:(proj1 (odivision_exists ob osa la)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)