proposition: Lemma expRat_rel_left_total : forall (r1 : Rat -> Prop) n, (exists r1', r1 r1') -> (forall x1 x2, r1 x1 -> r1 x2 -> x1 == x2) -> exists r3, expRat_rel r1 n r3.
proof: Proof. unfold expRat_rel in *. intuition. destruct H. exists (expRat x n). intuition. eapply expRat_eqRat_compat; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms