proposition: Lemma rNecS s : mprv s -> mprv (AG s).
proof: Proof. move => H. apply: rMP (H). apply: rAG_ind => //. drop. exact: rNec. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions