proposition: Theorem mask_correct' : forall xi yi x, contains (convert xi) x -> contains (convert (mask xi yi)) x.
proof: Proof. now intros xi [|yl yu] x Hx. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval