proposition: Lemma interpolation_prop2 n u v (f := simple_interpolation n u v): ratp n -> u <q v -> (forall x, n <=q x -> x <q (n +q \1q) -> (u <=q f x /\ f x <q v)) /\ (forall y, u <=q y -> y <q v -> exists x, [/\ n <=q x, x <q (n +q \1q) & y = f x]).
proof: Proof. move => pa pb; move:(interpolation_prop1 pa pb). rewrite -/f; move => [qa qb qc qd qe]. split. move => x xa xb; move: (qc _ xa (proj1 xb)) => [sa sb]; split => //. by rewrite - qb; apply: qe. move => y ya [yb yc]; move:(qd _ ya yb) => [x [xa xn yv]]. by exists x; split => //; split => //; dneg eq1; rewrite yv eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)