proposition: Theorem le_i_SSi : forall i:nat, i <= S (S i).
proof: Proof. Proof (fun i:nat => le_S (le_S (le_n i))). Definition compose {A B C : Type} : (A->B)->(B->C)->A->C := fun f g x => g (f x). Definition thrice {A:Type} (f:A->A) := compose f (compose f f). Lemma thrice_as_iter_3 {A:Type} (f: A -> A): thrice f = iterate f 3. Proof. reflexivity. Qed.
imports: ZArith List Arith ZArithRing