proposition: Lemma Zabs_mult : forall z p : Z, Z.abs (z * p) = (Z.abs z * Z.abs p)%Z.
proof: Proof. intros. case z. simpl in |- *. reflexivity. case p. simpl in |- *. reflexivity. intros. simpl in |- *. reflexivity. intros. simpl in |- *. reflexivity. case p. intro. simpl in |- *. reflexivity. intros. simpl in |- *. reflexivity. intros. simpl in |- *. reflexivity. Qed.
imports: Coq(Lia)