proposition: Lemma prelift_aux_fold_aux : forall Pt m n i j, j >= i -> j <= n + i -> prelift_aux m (prelift_aux n Pt i) j = prelift_aux (m + n) Pt i.
proof: Proof. induction Pt; unfold prelift; intros m n i j j_ge j_le; simpl. destruct (le_gt_dec i x); simpl. destruct (le_gt_dec j (x + n)); simpl. assert (x + (m + n) = x + n + m). lia. try_solve. lia. destruct (le_gt_dec j x); simpl. lia. try_solve. trivial. rewrite <- (IHPt m n (S i) (S j)); trivial. lia. lia. rewrite IHPt1; try_solve. rewrite IHPt2; try_solve. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)