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