proposition: Lemma sep__sep_points_lemma : Points_in_Partition sep__sep_part sep__sep_points.
proof: Proof. red in |- *; intros. split. unfold sep__sep_part in |- *; simpl in |- *. unfold sep__sep_fun, sep__sep_points in |- *. elim (le_lt_dec i 0); intro; simpl in |- *. apply leEq_transitive with (g i Hi). elim (Pts_part_lemma _ _ _ _ _ _ gP i Hi); intros; assumption. apply rht_leEq_Max. elim (le_lt_eq_dec _ _ (Nat.lt_le_incl _ _ Hi)); intro; simpl in |- *. eapply leEq_wdl. apply lft_leEq_Max. apply sep__sep_fun_i_wd; auto. exfalso; rewrite b1 in Hi; apply (Nat.lt_irrefl _ Hi). unfold sep__sep_part in |- *; simpl in |- *. unfold sep__sep_fun, sep__sep_points in |- *. elim (le_lt_dec (S i) 0); intro; simpl in |- *. exfalso; inversion a0. elim (le_lt_eq_dec _ _ Hi); intro; simpl in |- *. apply Max_leEq. apply less_leEq; apply sep__sep_mon_i; assumption. apply leEq_transitive with (P (S i) Hi). elim (gP i Hi); intros; auto. apply sep__sep_leEq. apply Max_leEq. unfold sep__sep_fun_i in |- *. elim (sep__sep_aux_lemma i); intro; simpl in |- *. apply leEq_transitive with (P (S i) Hi). apply shift_plus_leEq'. apply leEq_transitive with delta. astepl (delta [/]TwoNZ); apply less_leEq; apply pos_div_two'; exact RS_delta_pos. apply leEq_transitive with deltaP. apply RS_delta_deltaP. unfold deltaP in |- *; apply AntiMesh_lemma. elim (Partition_in_compact _ _ _ _ P (S i) Hi); intros; assumption. elim (Partition_in_compact _ _ _ _ P i (Nat.lt_le_incl _ _ Hi)); intros; assumption. elim (Pts_part_lemma _ _ _ _ _ _ gP i Hi); intros; assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions