proposition: Lemma Zdiv_elim : forall a b d : Z, d <> 0%Z -> Zdivides d a -> Zdivides d b -> (a / d)%Z = (b / d)%Z -> a = b.
proof: Proof. intros a b d Hd Ha Hb. elim Ha; clear Ha; intros x Ha; rewrite <- Ha. elim Hb; clear Hb; intros y Hb; rewrite <- Hb. repeat rewrite Zdiv_mult_cancel_rht; auto. intro Hxy; rewrite Hxy; auto. Qed.
imports: CoRN.model.Zmod.ZBasics