proposition: Lemma pjp_3 : forall (i : nat) Hi Hi', n < i -> partition_join_pts i Hi [=] fQ (i - S n) Hi'.
proof: Proof. intros; unfold partition_join_pts in |- *. elim le_lt_dec; intro; simpl in |- *. exfalso; apply Nat.le_ngt with i n; auto. cut (fQ _ (partition_join_aux' _ _ _ b0 Hi) [=] fQ _ Hi'). 2: apply HfQ'; auto. algebra. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)