proposition: Lemma Zdivides_opp_elim_lft : forall a b : Z, Zdivides a b -> Zdivides (- a) b.
proof: Proof. intros a b H. unfold Zdivides in H; elim H; intros q H_. exists (- q)%Z. rewrite Zmult_opp_opp. assumption. Qed.
imports: CoRN.model.Zmod.ZBasics