proposition: Theorem ZquotientPos : forall z1 z2 : Z, (0 <= z1)%Z -> (0 <= z2)%Z -> (0 <= Zquotient z1 z2)%Z.
proof: Proof. intros z1 z2 H H0; case (Z.eq_dec z2 0); intros Z1. rewrite Z1; red in |- *; case z1; simpl in |- *; auto; intros; red in |- *; intros; discriminate. case (ZquotientProp z1 z2); auto; intros r (H1, (H2, H3)). case (Zle_or_lt 0 (Zquotient z1 z2)); auto; intros Z2. contradict H3; apply Zle_not_lt. replace r with (z1 - Zquotient z1 z2 * z2)%Z; [ idtac | pattern z1 at 1 in |- *; rewrite H1; ring ]. repeat rewrite Z.abs_eq; auto. pattern z2 at 1 in |- *; replace z2 with (0 + 1 * z2)%Z; [ idtac | ring ]. unfold Zminus in |- *; apply Z.le_trans with (z1 + 1 * z2)%Z; auto with zarith. apply Zplus_le_compat_l. rewrite Zopp_mult_distr_l. apply Zle_Zmult_comp_r; auto with zarith. unfold Zminus in |- *; rewrite Zopp_mult_distr_l; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz