proposition: Lemma Positive_prod : ∀ {n m}, Positive n → Positive m → Positive (n * m).
proof: Proof. intros n m hn hm. unfold Positive in *. eapply leq_trans. 2: eapply leq_pmull. all: auto. Qed.
imports: Coq(Utf8 Lia) mathcomp(ssreflect eqtype ssrbool ssrnat) extructures(ord fset) Equations(Equations)