proposition: Lemma times_Zmult : forall p q, Zpos (p * q)%P = (p * q)%Z.
proof: Proof. intros p q;generalize q p;clear p q. induction q;destruct p; unfold times; try fold (times p q); autorewrite with zmisc; try rewrite IHq; ring. Qed.
imports: ZArith Lia