proposition: Theorem list_hybrid_close_h : (forall n c, | (evalDist (LH_Gn n) c) - (evalDist (LH_Gn (S n)) c) | <= F n) -> forall x n c, | (evalDist (LH_Gn n) c) - (evalDist (LH_Gn (n + x)) c) | <= sumList (map (plus n) (allNatsLt x)) F.
proof: Proof. Local Opaque evalDist. induction x; intuition; simpl in *. rewrite plus_0_r. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. intuition. eapply rat0_le_all. eapply leRat_trans. eapply ratDistance_le_trans. eapply H. assert (n + S x = S n + x)%nat. lia. rewrite H0. clear H0. eapply IHx. rewrite map_app. simpl. Admitted. Theorem skipn_length_nil : forall (A : Type)(ls : list A)(n : nat), n >= length ls -> skipn n ls = nil. induction ls; intuition; simpl in *. destruct n; simpl in *; trivial. destruct n; simpl in *. lia. eapply IHls. lia. Qed.
imports: FCF CompFold