proposition: Lemma sub_propagate_l : forall prec, propagate_l (sub prec).
proof: Proof. intros prec xi yi; destruct xi; destruct yi; [easy..|]. now unfold convert; case (_ && _). Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval