proposition: Lemma F1_F0_2 : dominates_from 2 (F_ 1) (F_ 0).
proof: Proof. intros i Hi; rewrite F_S_rw; cbn. pattern i at 2; generalize Hi; induction 1. - cbn; auto with arith. - Locate succ_lt_mono. rewrite <- PeanoNat.Nat.succ_lt_mono. cbn. transitivity (S (iterate (fun n : nat => S n) m m )); auto. rewrite <- PeanoNat.Nat.succ_lt_mono. apply iterate_mono. + intros x y Hxy;auto with arith. + auto with arith. Qed.
imports: Coq(ArithRing Lia Arith)