proposition: Lemma Zdiv_mult_cancel_lft : forall a b : Z, a <> 0%Z -> (a * b / a)%Z = b.
proof: Proof. intros a b. case a. auto with zarith. intros p _. apply (Zdiv_quotient_unique (Zpos p * b) (Zpos p) (Zpos p * b / Zpos p) ((Zpos p * b) mod Zpos p) b 0). rewrite (Zmult_comm (Zpos p * b / Zpos p) (Zpos p)). apply Z_div_mod_eq_full. apply Z_mod_lt; auto with zarith. rewrite Zplus_0_r; auto with zarith. auto with zarith. intros p _. fold (- Zpos p)%Z in |- *. rewrite Zdiv_Zopp. cut ((- Zpos p * b / Zpos p)%Z = (- b)%Z); auto with zarith. unfold Z.opp in |- *; fold (- b)%Z in |- *. apply (Zdiv_quotient_unique (Zneg p * b) (Zpos p) (Zneg p * b / Zpos p) ((Zneg p * b) mod Zpos p) (- b) 0). rewrite (Zmult_comm (Zneg p * b / Zpos p) (Zpos p)). apply Z_div_mod_eq_full. apply Z_mod_lt; auto with zarith. rewrite Zplus_0_r; rewrite Zmult_opp_comm; fold (- Zpos p)%Z in |- *; auto with zarith. auto with zarith. rewrite Zmult_opp_comm. apply Zmod_mult_cancel_lft. Qed.
imports: CoRN.model.Zmod.ZBasics