proposition: Lemma sep__part_pts_lemma : forall (i : nat) Hi Hi', sep__part_pts i Hi[=]g (pred (sep__part_h (S i))) Hi'.
proof: Proof. intros; unfold sep__part_pts in |- *. apply gP'; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)