proposition: Lemma mediant_3 : forall a b m n m' n' : Z, (0 <= a * m + b * n)%Z -> (0 <= a * m' + b * n')%Z -> (0 <= a * (m + m') + b * (n + n'))%Z.
proof: Proof. intros. replace (a * (m + m') + b * (n + n'))%Z with (a * m + b * n + (a * m' + b * n'))%Z. apply Zplus_le_0_compat. assumption. assumption. ring. Qed.
imports: Coq(Lia)