proposition: Lemma Zquot_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)÷(c*b) = a÷b.
proof: Proof. intros. rewrite (Z.mul_comm c b). zero_or_not b. rewrite (Z.mul_comm b c). apply Z.quot_mul_cancel_l; auto. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms