proposition: Lemma nat_of_mul_pos p q : (p * q)%positive = p * q :> nat.
proof: Proof. elim: p => [p IHp|p IHp|] /=; rewrite ?mul1n //; by rewrite ?nat_of_add_pos /= !natTrecE IHp doubleMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring