proposition: Lemma partition_join_finish : forall H, partition_join_fun (S (n + m)) H [=] b.
proof: Proof. intro. unfold partition_join_fun in |- *. elim le_lt_dec; intro; simpl in |- *. exfalso; apply Nat.nle_succ_diag_l with n; apply Nat.le_trans with (S (n + m)); auto with arith. apply eq_transitive_unfolded with (Q _ (le_n _)). apply prf1; auto with arith. apply finish. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)