proposition: Lemma iterFsubn m n : m <= n -> iter m F set0 \subset iter n F set0.
proof: Proof. Proof using monoF. elim : n; first by rewrite leqn0 ; move/eqP->. move => n IH. rewrite leq_eqVlt; case/orP; first by move/eqP<-. move/IH => /= IHe. apply: subset_trans IHe _. exact:iterFsub. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)