proposition: Theorem mask_correct : extension_2 Xmask mask.
proof: Proof. intros xi [|yl yu] x [|y] Hx Hy; try easy. now revert Hy; simpl; case (_ && _). Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval