proposition: Lemma abs_minus_pos : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (x >= y)%Z -> Z.abs_nat (x - y) = Z.abs_nat x - Z.abs_nat y.
proof: Proof. intros. elim (Z_of_nat_complete x). intros nx Hx. elim (Z_of_nat_complete y). intros ny Hy. elim (Z_of_nat_complete (x - y)). intros d Hd. rewrite Hx. rewrite Hy. rewrite <- Znat.inj_minus1. rewrite abs_inj. rewrite abs_inj. rewrite abs_inj. reflexivity. rewrite (isnat_inj_abs x nx). rewrite (isnat_inj_abs y ny). apply lezle. assumption. assumption. apply Z.ge_le. assumption. assumption. assumption. unfold Zminus in |- *. apply Zle_left. apply Z.ge_le. assumption. assumption. assumption. Qed.
imports: ZArith EqNat lemmas