proposition: Theorem Z2Nat_inj_mul_pos_r : ∀ n m, Z.to_nat (n * Zpos m) = (Z.to_nat n * Pos.to_nat m)%nat.
proof: Proof. intros n m. destruct n as [| n| ]; [ reflexivity | simpl | reflexivity ]. rewrite Pos2Nat.inj_mul; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz