proposition: Theorem ratSubtract_le : forall r1 r2 d, r1 <= d -> ratSubtract r1 r2 <= d.
proof: Proof. intuition. unfold ratSubtract. rattac. arithNormalize. apply minus_le. rewrite <- (Nat.mul_assoc n). rewrite (Nat.mul_comm x0). rewrite Nat.mul_assoc. apply Nat.mul_le_mono; trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms