fact: Definition posnatMult(p1 p2 : posnat) : posnat := match (p1, p2) with | (exist _ n1 pf1, exist _ n2 pf2) => (exist (fun n => n > 0) (n1 * n2) (mult_gt_0 pf1 pf2)) end.
imports: Arith micromega.Lia Coq.NArith.BinNat