proposition: Lemma iter_fix T (F : T -> T) x k n : iter k F x = iter k.+1 F x -> k <= n -> iter n F x = iter n.+1 F x.
proof: Proof. move => e. elim: n. rewrite leqn0. by move/eqP<-. move => n IH. rewrite leq_eqVlt; case/orP; first by move/eqP<-. move/IH => /= IHe. by rewrite -!IHe. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)