proposition: Lemma mediant_2 : forall m n m' n' : Z, (m' * n < m * n')%Z -> (m' * (n + n') < (m + m') * n')%Z.
proof: Proof. intros. rewrite Zmult_plus_distr_l. rewrite Zmult_plus_distr_r. apply Zplus_lt_compat_r. assumption. Qed.
imports: Coq(Lia)