proposition: Lemma iterFsub n : iter n F set0 \subset iter n.+1 F set0.
proof: Proof. Proof using monoF. elim: n => //=; first by rewrite sub0set. move => n IH /=. by apply: monoF. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)