proposition: Lemma abs_mult : forall x y : Z, Z.abs_nat (x * y) = Z.abs_nat x * Z.abs_nat y.
proof: Proof. simple induction x. simpl in |- *. intro. reflexivity. intro. simple induction y. simpl in |- *. rewrite <- mult_n_O. reflexivity. intro. simpl in |- *. rewrite <- nat_of_P_mult_morphism. reflexivity. simpl in |- *. intro. rewrite <- nat_of_P_mult_morphism. reflexivity. intro. simple induction y. simpl in |- *. rewrite <- mult_n_O. reflexivity. intro. unfold Z.abs_nat in |- *. simpl in |- *. rewrite <- nat_of_P_mult_morphism. reflexivity. intro. unfold Z.abs_nat in |- *. simpl in |- *. rewrite <- nat_of_P_mult_morphism. reflexivity. Qed.
imports: ZArith EqNat lemmas