proposition: Lemma ord_ext_div_unique a b x y z x' y' z': \2o <=o a -> ordinalp b -> ord_ext_div_pr a b x y z -> ord_ext_div_pr a b x' y' z' -> [/\ x=x', y=y' & z=z'].
proof: Proof. move=> pa ob. have oa:= proj32 pa. have aux: forall x y z, ord_ext_div_pr a b x y z -> (a ^o x <=o b /\ b <o a ^o (osucc x)). move => u v w [ou ov ow [-> r1 r2 r3]]; move: (OS_pow oa ou) => op; split. apply:(oleT (oprod_Mle1 op r3)); apply:(osum_Mle0 (OS_prod2 op ov) ow). apply:(olt_leT (osum_Meqlt r1 (OS_prod2 op ov))). rewrite - (oprod2_succ op ov) (opow_succ oa ou); apply:oprod_Meqle => //. by apply /oleSltP. move => p1 p2. move: (aux _ _ _ p1) (aux _ _ _ p2) => [p3 p4][p5 p6]. move: p1 p2 => [ox oy oz [bv r1 r2 r3]][ox' oy' oz' [bv' r1' r2' r3']]. have sx: x = x'. move: (proj1 (opow_normal pa)) => h. apply: (sincr_bounded_unique h ox ox' p3 p4 p5 p6). rewrite - sx in bv' r1'. have p7 : (odiv_pr0 b (a^o x) y z) by split. have p8 : (odiv_pr0 b (a^o x) y' z') by split. by move: (odivision_unique ob (OS_pow oa ox) p7 p8) => [e1 e2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)