proposition: Lemma sep__part_pts_in_Partition : Points_in_Partition sep__part sep__part_pts.
proof: Proof. red in |- *; intros i Hi. set (H := sep__part_h_mon_3 _ _ (eq_ind (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) ( fun n0 : nat => n0 < n) (sep__part_fun_bnd' i (Nat.lt_le_incl _ _ Hi) Hi) (sep__part_h i) (sep__part_fun_i i (Nat.lt_le_incl _ _ Hi) Hi)) (Nat.lt_succ_diag_r i)) in *. set (H0 := eq_sym (Nat.lt_succ_pred (sep__part_h i) (sep__part_h (S i)) H)) in *. set (H' := eq_ind (sep__part_h (S i)) (fun j : nat => j <= n) ( sep__part_h_bnd (S i)) (S (pred (sep__part_h (S i)))) H0) in *. elim (gP _ H'); intros. simpl in |- *; unfold sep__part_pts in |- *. split. eapply leEq_transitive. 2: apply a0. apply Partition_mon; apply le_2. rewrite sep__part_fun_i; assumption. eapply leEq_transitive. apply b0. apply Partition_mon. rewrite <- H0. apply sep__part_fun_i'. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)