proposition: Lemma int_exPi : forall i, exists j, fst (F' j) <= i /\ i < snd (F' j).
proof: Proof. intros i. induction i. exists 0. simpl. destruct (HFi 0); rewrite H. lia. destruct IHi as [k Hk]. assert (HSi : S i <= snd (F' k)). lia. destruct (le_lt_or_eq HSi). exists k. intuition. exists (S k). simpl. rewrite H. split. lia. destruct (HFi (S k)). rewrite H0. lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)