proposition: Lemma cquo_simplify a b c: natp a -> natp b -> natp c -> b <> \0c -> c <> \0c -> (a *c c) %/c (b *c c) = a %/c b.
proof: Proof. move=> aN bN cN bnz cnz. have [qN rN []] := (cdivision aN bN bnz). set q:= (a %/c b); set r := a %%c b. move=> e1 lrb; symmetry. move: (NS_prod aN cN)(NS_prod bN cN)(NS_prod (NS_rem b aN) cN) => p1 p2 p3. have dv: (cdivision_prop (a *c c) (b *c c) q (r *c c)). split. rewrite (cprodC b c) - cprodA (cprodC c _). by rewrite - cprodDl e1. by rewrite (cprodC b c) cprodC; apply: cprod_Meqlt. exact (proj1 (cquorem_pr p1 p2 qN p3 dv)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)