proposition: Lemma partition_join_Pts_wd : forall i j, i = j -> forall Hi Hj, partition_join_pts i Hi [=] partition_join_pts j Hj.
proof: Proof. intros. elim (le_lt_dec i n); intro. elim (le_lt_eq_dec _ _ a0); intro. cut (j < n); [ intro | rewrite <- H; assumption ]. eapply eq_transitive_unfolded. apply pjp_1 with (Hi' := a1). eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply pjp_1 with (Hi' := H0). apply HfP'; auto. cut (j = n); [ intro | rewrite <- H; assumption ]. eapply eq_transitive_unfolded. apply pjp_2; auto. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply pjp_2; auto. algebra. cut (n < j); [ intro | rewrite <- H; assumption ]. cut (i - S n < m); [ intro | lia ]. cut (j - S n < m); [ intro | lia ]. eapply eq_transitive_unfolded. apply pjp_3 with (Hi' := H1); assumption. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply pjp_3 with (Hi' := H2); assumption. apply HfQ'; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)