proposition: Lemma cdivision_unique a b q r q' r': natp a -> natp b -> natp q -> natp r -> natp q' -> natp r' -> b <> \0c -> cdivision_prop a b q r -> cdivision_prop a b q' r' -> (q = q' /\ r =r').
proof: Proof. move=> aN bN qN rN q'N r'N nbz. move /(cdivision_prop_alt aN bN qN rN nbz)=> [le1 lt1 e1]. move /(cdivision_prop_alt aN bN q'N r'N nbz)=> [le2 lt2 e2]. suff : q = q' by move=> h; split => //; rewrite e1 e2 h. move: (cprod_lt2l bN q'N (NS_succ qN) (cle_ltT le2 lt1)). move: (cprod_lt2l bN qN (NS_succ q'N) (cle_ltT le1 lt2)). by move /(cltSleP q'N) => pa /(cltSleP qN) => /(cleA pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)