proposition: Lemma pjf_2 : forall (i : nat) Hi, i = n -> partition_join_fun i Hi [=] c.
proof: Proof. intros; unfold partition_join_fun in |- *. generalize Hi; clear Hi. rewrite H; clear H; intro. elim le_lt_dec; intro; simpl in |- *. apply finish. exfalso; apply Nat.lt_irrefl with n; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)