proposition: Lemma Zdivides_opp_elim_rht : 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 Zopp_mult_distr_l_reverse. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics