proposition: Lemma pjp_2 : forall (i : nat) Hi, i = n -> partition_join_pts i Hi [=] c.
proof: Proof. intros; unfold partition_join_pts in |- *. elim le_lt_dec; intro; simpl in |- *. elim le_lt_eq_dec; intro; simpl in |- *. exfalso; rewrite H in a1; apply (Nat.lt_irrefl _ a1). algebra. exfalso; rewrite H in b0; apply (Nat.lt_irrefl _ b0). Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)