proposition: Lemma partition_join_Pts_in_partition : Points_in_Partition partition_join partition_join_pts.
proof: Proof. red in |- *; intros. rename Hi into H. cut (forall H', compact (partition_join i (Nat.lt_le_incl _ _ H)) (partition_join (S i) H) H' (partition_join_pts i H)); auto. unfold partition_join in |- *; simpl in |- *. unfold partition_join_fun in |- *. elim le_lt_dec; elim le_lt_dec; intros; simpl in |- *. elim (le_lt_eq_dec _ _ a1); intro. elim (HfP _ a2); intros. apply compact_wd with (fP i a2). 2: apply eq_symmetric_unfolded; apply pjp_1. split. eapply leEq_wdl. apply a3. apply prf1; auto. eapply leEq_wdr. apply b0. apply prf1; auto. exfalso; clear H'; rewrite b0 in a0; apply (Nat.nle_succ_diag_l _ a0). cut (i = n); [ intro | clear H'; apply Nat.le_antisymm; auto with arith ]. generalize H a0 b0 H'; clear H' a0 b0 H; rewrite H0; intros. apply compact_wd with c. 2: apply eq_symmetric_unfolded; apply pjp_2; auto. split. apply eq_imp_leEq; apply finish. apply eq_imp_leEq; apply eq_symmetric_unfolded. cut (forall H, Q (n - n) H [=] c); auto. cut (n - n = 0); [ intro | auto with arith ]. rewrite H1; intros; apply start. exfalso; apply Nat.le_ngt with n i; auto with arith. elim (HfQ _ (partition_join_aux' _ _ _ b1 H)); intros. apply compact_wd with (fQ _ (partition_join_aux' _ _ _ b1 H)). 2: apply eq_symmetric_unfolded; apply pjp_3; assumption. split. eapply leEq_wdl. apply a0. apply prf1; auto. eapply leEq_wdr. apply b2. apply prf1; rewrite <- Nat.sub_succ_l; auto with arith. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)