proposition: Lemma iterFsub n m : n <= m -> iter n F fset0 `<=` iter m F fset0.
proof: Proof. Proof using F_mono. move/subnK<-. elim: (m-n) => {m} [|m IHm]; first exact: subxx. apply: sub_trans IHm _. rewrite addSn. exact: iterFsub1. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)