proposition: Lemma Zmult_le_1_compat : forall a b, 1 <= a -> 1 <= b -> 1 <= a * b.
proof: Proof. intros a b. replace a with (1 + (a - 1)) by lia. replace b with (1 + (b - 1)) by lia. generalize (a - 1). generalize (b - 1). intros c d. intros. assert (0 <= c) by lia. assert (0 <= d) by lia. ring_simplify. assert (0 <= d * c) by auto with *. lia. Qed.
imports: ZArith Lia Znumtheory