proposition: Lemma abs_plus_pos : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> Z.abs_nat (x + y) = Z.abs_nat x + Z.abs_nat y.
proof: Proof. simple induction x. simpl in |- *. intros. reflexivity. intro. simple induction y. simpl in |- *. rewrite <- plus_n_O. intros. reflexivity. simpl in |- *. intros. apply nat_of_P_plus_morphism. intros. unfold Z.le in H0. simpl in H0. elim H0. reflexivity. intros. unfold Z.le in H. simpl in H. elim H. reflexivity. Qed.
imports: ZArith EqNat lemmas