proposition: Lemma AR_mono : mono AR_fun.
proof: Proof. move => X Y S. apply: setUS. apply/subsetP => x; rewrite !inE. case (q x) => //= ?. apply/forall_inP => y xy. apply: (subsetP S). by apply/forall_inP : y xy. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)