proposition: Lemma Zdiv_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)/(c*b) = a/b.
proof: Proof. intros a b c ?. rewrite (Z.mul_comm c b); zero_or_not b. rewrite (Z.mul_comm b c). apply Z.div_mul_cancel_l; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms