proposition: Lemma odivision_unique a b q r q' r': ordinalp a -> ordinalp b -> odiv_pr0 a b q r -> odiv_pr0 a b q' r' -> (q = q' /\ r = r').
proof: Proof. move => oa ob pa pb. have aux: forall q r, odiv_pr0 a b q r -> (b *o q <=o a /\ a <o b *o (osucc q)). move=> q1 r1 [oq or -> rb]; rewrite (oprod2_succ ob oq). split; first by apply:(osum_Mle0 (OS_prod2 ob oq) or). apply:(osum_Meqlt rb (OS_prod2 ob oq)). move: (aux _ _ pa) (aux _ _ pb) => [s1 s2] [s3 s4]. pose h y := b *o y. move: pa pb => [oq or e1 rb] [oq' or' e2 _]. have bp:= (ole_ltT (ole0x or) rb). have sii: sincr_ofs (oprod2 b). by move => u v uv; apply: oprod_Meqlt. move: (sincr_bounded_unique sii oq oq' s1 s2 s3 s4). move => sq; split => //; rewrite e1 sq in e2. exact: (osum2_simpl or or' (OS_prod2 ob oq') e2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)