proposition: Lemma oquoremP2 a b q r: ordinalp a -> \0o <o b -> odiv_pr0 a b q r -> q = (oquo a b) /\ r = (orem a b).
proof: Proof. move => pa pb pc. move:(oquoremP pa pb) => pd. exact (odivision_unique pa (proj32_1 pb) pc pd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)