proposition: Lemma ratSubtract_assoc_le : forall r1 r2 r3, ratSubtract r1 (ratSubtract r2 r3) <= (ratSubtract r1 r2) + r3.
proof: Proof. unfold ratSubtract. rattac. arithNormalize. remember (n * x * x0 * x1 * x * x0)%nat as a. assert (n1 * x0 * x1 * x1 * x * x0 = n1 * x1 * x0 * x1 * x * x0)%nat. do 5 arithSimplify. rewrite H. assert (n2 * x * x1 * x1 * x * x0 = n2 * x1 * x * x1 * x * x0)%nat. do 5 arithSimplify. rewrite H0. remember (n1 * x1 * x0 * x1 * x * x0)%nat as b. remember (n2 * x1 * x * x1 * x * x0)%nat as c. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms