proposition: Lemma ratAdd_any_leRat_l : forall r1 r2 r3, r1 <= r3 -> r1 <= r3 + r2.
proof: Proof. rattac. arithNormalize. assert (n * x * x0 <= n0 * x0 * x1)%nat. rewrite (Nat.mul_comm (n0 * x0) x1). rewrite Nat.mul_assoc. apply Nat.mul_le_mono; trivial. rewrite (Nat.mul_comm x1). trivial. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono; eauto. apply le_0_n. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms