proposition: Lemma ratAdd_leRat_compat_l : forall r1 r2 r3, leRat r1 r2 -> r1 + r3 <= r2 + r3.
proof: Proof. rattac. unfold leRat, bleRat in *. rattac. arithNormalize. apply Nat.add_le_mono. apply Nat.mul_le_mono; trivial. repeat rewrite <- Nat.mul_assoc. repeat rewrite (Nat.mul_comm x0). repeat rewrite Nat.mul_assoc. apply Nat.mul_le_mono; trivial. apply Nat.mul_le_mono; trivial. rewrite <- Nat.mul_assoc. rewrite (Nat.mul_comm x1). rewrite Nat.mul_assoc. apply Nat.mul_le_mono; trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms