proposition: Lemma inj_abs_pos : forall x : Z, (x >= 0)%Z -> Z_of_nat (Z.abs_nat x) = x.
proof: Proof. simple induction x. reflexivity. intros. simpl in |- *. induction p as [p Hrecp| p Hrecp| ]. rewrite BinInt.Zpos_xI. rewrite <- Hrecp. replace (nat_of_P (xI p)) with (S (2 * nat_of_P p)). rewrite Znat.inj_S. rewrite Znat.inj_mult. rewrite Hrecp. simpl in |- *. reflexivity. apply Z.le_ge. apply Zorder.Zle_0_pos. replace 2 with (nat_of_P 2). rewrite <- nat_of_P_mult_morphism. simpl in |- *. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ. rewrite P_of_succ_nat_o_nat_of_P_eq_succ. simpl in |- *. reflexivity. simpl in |- *. reflexivity. apply Z.le_ge. apply Zorder.Zle_0_pos. rewrite BinInt.Zpos_xO. rewrite <- Hrecp. replace (nat_of_P (xO p)) with (2 * nat_of_P p). rewrite Znat.inj_mult. rewrite Hrecp. simpl in |- *. reflexivity. apply Z.le_ge. apply Zorder.Zle_0_pos. replace 2 with (nat_of_P 2). rewrite <- nat_of_P_mult_morphism. simpl in |- *. reflexivity. simpl in |- *. reflexivity. apply Z.le_ge. apply Zorder.Zle_0_pos. reflexivity. intros. elim H. simpl in |- *. reflexivity. Qed.
imports: ZArith EqNat lemmas