proposition: Lemma Part_Mesh_List_lemma : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n) x, member x (Part_Mesh_List P) -> {i : nat | {Hi : i <= n | {Hi' : S i <= n | x [=] P _ Hi'[-]P _ Hi}}}.
proof: Proof. intro; induction n as [| n Hrecn]. simpl in |- *; intros. easy. intros a b Hab P x H. simpl in H; elim H; clear H; intro H0. elim (Hrecn _ _ _ _ _ H0); clear Hrecn. intros i H; elim H; clear H. intros Hi H; elim H; clear H. intros Hi' H. simpl in H. exists i; exists (le_S _ _ Hi); exists (le_S _ _ Hi'). eapply eq_transitive_unfolded. apply H. apply cg_minus_wd; apply prf1; auto. exists n. exists (le_S _ _ (le_n n)). exists (le_n (S n)). eapply eq_transitive_unfolded. apply H0. apply cg_minus_wd; apply prf1; auto. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)