proposition: Lemma expRat_rel_func : forall (r : Rat -> Prop) v1 v2 n, expRat_rel r n v1 -> expRat_rel r n v2 -> (forall x1 x2, r x1 -> r x2 -> x1 == x2) -> (exists r', r r') -> v1 == v2.
proof: Proof. unfold expRat_rel in *. intuition. destruct H2. rewrite H; eauto. rewrite H0; eauto. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms