proposition: Lemma mult_le_compat_r_iff_h : forall n2 n3 n1, n1 > O -> (n2 * n1 <= n3 * n1)%nat -> (n2 <= n3)%nat.
proof: Proof. induction n2; destruct n3; intuition idtac; simpl in *. lia. exfalso. remember (n2 * n1)%nat as x. lia. eapply le_n_S. eapply IHn2; eauto. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia