proposition: Lemma pjp_1 : forall (i : nat) Hi Hi', partition_join_pts i Hi [=] fP i Hi'.
proof: Proof. intros; unfold partition_join_pts in |- *. elim le_lt_dec; intro; simpl in |- *. elim le_lt_eq_dec; intro; simpl in |- *. algebra. exfalso; rewrite b0 in Hi'; apply (Nat.lt_irrefl _ Hi'). exfalso; apply Nat.le_ngt with i n; auto with arith. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)