proposition: Lemma leFiter {T : UU} (F : T -> T) (t : T) (n : nat) : leF F t (iteration F n t).
proof: Proof. intros. induction n as [ | n IHn ]. - apply leF_O. - simpl. apply leF_S. assumption. Defined.
imports: UniMath.Foundations.NaturalNumbers