proposition: Lemma minoration : F_ 2 >>s exp2.
proof: Proof. eapply dominates_trans_strong. 2: eapply LF2. exists 2. intros i. induction 1. compute. auto with arith. simpl. rewrite <- mult_n_Sm. ring_simplify. rewrite <- Nat.mul_assoc. generalize IHle; generalize (exp2 m * m); generalize (exp2 m). clear IHle. intros. lia. Qed.
imports: Coq(ArithRing Lia Arith)