proposition: Lemma Zmod_mult_cancel_lft : forall a b : Z, ((a * b) mod a)%Z = 0%Z.
proof: Proof. intros a b. case a. auto with zarith. intro p. apply Zmod0_Zdivides_pos. auto with zarith. apply Zdivides_mult_elim_rht. apply Zdivides_ref. intro p. apply Zmod0_Zdivides. auto with zarith. apply Zdivides_mult_elim_rht. apply Zdivides_ref. Qed.
imports: CoRN.model.Zmod.ZBasics