proposition: Lemma big_induction : forall i, (mono (F_ i) * (F_ (S i) >>s F_ i) * (F_ i >>s id_nat))%type.
proof: Proof. induction i. repeat split. apply mono_F0. exists 1. intros x Hx; rewrite LF1, LF0. lia. exists 0. intros x Hx. simpl. unfold id_nat;auto with arith. destruct IHi as [[X Y] Z];repeat split. apply mono_mono;auto. apply dom_dom;auto. eapply dominates_trans_strong; eauto. apply mono_mono;auto. eapply dominates_trans_strong; eauto. Defined.
imports: Coq(ArithRing Lia Arith)