proposition: Lemma leqif_mul m1 n1 C1 m2 n2 C2 : m1 <= n1 ?= iff C1 -> m2 <= n2 ?= iff C2 -> m1 * m2 <= n1 * n2 ?= iff (n1 * n2 == 0) || (C1 && C2).
proof: Proof. case: n1 => [|n1] le1; first by case: m1 le1 => [|m1] [_ <-] //. case: n2 m2 => [|n2] [|m2] /=; try by case=> // _ <-; rewrite !muln0 ?andbF. have /leq_pmul2l-/mono_leqif<-: 0 < n1.+1 by []. by apply: leqif_trans; have /leq_pmul2r-/mono_leqif->: 0 < m2.+1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring