proposition: Lemma in_sub_has (T:eqType) (a1 a2 : pred T) s : {in s, subpred a1 a2} -> has a1 s -> has a2 s.
proof: Proof. move => H /hasP [x ins Ha]. apply/hasP. exists x => //. exact: H. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)