proposition: Lemma propagate_extension : forall fi f, I.extension (Xbind f) fi -> propagate fi.
proof: Proof. intros fi f Hf xi H. specialize (Hf xi Xnan). rewrite H in Hf. specialize (Hf I). clear -Hf. now destruct I.convert. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic