proposition: Theorem ZdividesZquotient : forall n m : Z, m <> 0%Z -> Zdivides n m -> n = (Zquotient n m * m)%Z.
proof: Proof. intros n m H' H'0. case H'0; intros z1 Hz1. case (ZquotientProp n m); auto; intros z2 (Hz2, (Hz3, Hz4)). cut (z2 = 0%Z); [ intros H1; pattern n at 1 in |- *; rewrite Hz2; rewrite H1; ring | idtac ]. cut (z2 = ((z1 - Zquotient n m) * m)%Z); [ intros H2 | idtac ]. case (Z.eq_dec (z1 - Zquotient n m) 0); intros H3. rewrite H2; rewrite H3; ring. contradict Hz4. replace (Z.abs m) with (1 * Z.abs m)%Z; [ idtac | ring ]. apply Zle_not_lt; rewrite H2. rewrite Zabs_Zmult; apply Zle_Zmult_comp_r; lia. rewrite Zmult_minus_distr_r; rewrite (Zmult_comm z1); rewrite <- Hz1; (pattern n at 1 in |- *; rewrite Hz2); ring. Qed.
imports: Reals ZArith List PeanoNat Psatz