proposition: Lemma ratAdd_rel_left_total : forall (r1 r2: Rat -> Prop), (exists r1', r1 r1') -> (exists r2', r2 r2') -> (forall x1 x2, r1 x1 -> r1 x2 -> x1 == x2) -> (forall x1 x2, r2 x1 -> r2 x2 -> x1 == x2) -> exists r3, ratAdd_rel r1 r2 r3.
proof: Proof. unfold ratAdd_rel in *. intuition. destruct H. destruct H0. exists (x + x0). intuition. eapply ratAdd_eqRat_compat; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms