proposition: Lemma Zmod0_Zopp : forall a b : Z, b <> 0%Z -> (a mod b)%Z = 0%Z -> (a mod - b)%Z = 0%Z.
proof: Proof. intros a b. generalize (Z_mod_lt (Z.abs a) (Z.abs b)). case a. case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *; auto with zarith. case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *. auto with zarith. intros p q. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. intros Hlt Hp HR; rewrite HR; auto with zarith. intros p q. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. case R. auto with zarith. intro r'; intros H0 H1 H2. enough (Zpos r' = Zpos p) by auto with zarith. fold (- Zpos p)%Z in H2. auto with zarith. intro r'; intros H0 H1 H2. elim H0; auto with zarith. case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *. auto with zarith. intros p q. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. case R; intros r' H0; intros; try (cut (Zpos r' = Zpos p); elim H0); auto with zarith. intros p q. elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R. case R; intros; try discriminate; try tauto. Qed.
imports: CoRN.model.Zmod.ZBasics