proposition: Lemma ratSubtract_partition_leRat : forall r3 r1 r2 d1 d2, ratSubtract r1 r3 <= d1 -> ratSubtract r3 r2 <= d2 -> ratSubtract r1 r2 <= d1 + d2.
proof: Proof. intuition. case_eq (bleRat r3 r1); intuition. case_eq (bleRat r2 r3); intuition. rewrite ratSubtract_partition; eauto. rewrite ratAdd_comm. eapply ratAdd_leRat_compat; intuition. eapply bleRat_total in H2. rewrite ratAdd_0_r. eapply ratAdd_leRat_compat. eapply leRat_trans; eauto. eapply ratSubtract_leRat; intuition. eapply rat0_le_all. apply bleRat_total in H1. case_eq (bleRat r2 r3); intuition. rewrite ratAdd_0_l. eapply ratAdd_leRat_compat. eapply rat0_le_all. eapply leRat_trans; eauto. eapply ratSubtract_leRat; intuition. apply bleRat_total in H2. rewrite ratSubtract_0. eapply rat0_le_all. eapply leRat_trans; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms