proposition: Theorem mult_gt_zero_if : forall (a b : nat), a * b > 0 -> (a > 0 /\ b > 0).
proof: Proof. induction a; induction b; lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms