proposition: Lemma inv_propagate : forall prec, propagate (I.inv prec).
proof: Proof. intros prec. apply propagate_extension with (1 := I.inv_correct prec). Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic