Tengo las siguientes definiciones: (definición de enteros positivos como un subtipo de nat)

Definition Z_pos_filter (p: nat) : bool :=
  if (beq_nat p 0) then false else true.
Definition Z_pos: Set := {n : nat | is_true (Z_pos_filter n) }.

Definition Z_pos__N (p: Z_pos): nat := proj1_sig p.

Definition Z_pos_mult (p q: Z_pos): Z_pos.
destruct (Z_pos_filter (Z_pos__N p * Z_pos__N q)) eqn:prf.
- exact ((exist _ (Z_pos__N p * Z_pos__N q) prf)).
- assert (forall n: nat, S n <> 0) by (intros; omega).
  assert (forall a b: nat, a <> 0 /\ b <> 0 -> a * b <> 0).
  { intros. destruct a, b. omega. omega. omega. simpl. apply H. }
  assert (forall r: Z_pos, Z_pos__N r <> 0) by apply Z_pos_nonzero_N.
  assert (Z_pos__N p * Z_pos__N q <> 0) by (apply H0; split; apply H1).
  unfold Z_pos_filter in prf.
  rewrite <- beq_nat_false_iff in H2.
  rewrite H2 in prf. inversion prf.
Defined.

Pero me quedé en mostrar que laZ_pos_mult es compatible con los números naturales de multiplicación b / w:

Lemma compat: forall p q: Z_pos, Z_pos__N (Z_pos_mult p q) = Z_pos__N p * Z_pos__N q.

¿Como puedo resolver esto