proposition: Lemma pjf_2' : forall (i : nat) Hi, i = S 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 |- *. exfalso; apply (Nat.nle_succ_diag_l _ a0). cut (forall H, Q (n - n) H [=] c); auto. cut (n - n = 0); [ intro | auto with arith ]. rewrite H; intros; apply start. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)