proposition: Lemma prelower_prelift_aux : forall Pt i j k, k >= j -> k <= i + j + 1 -> prelift_aux i Pt j = prelower_aux (prelift_aux (i + 1) Pt j) k.
proof: Proof. induction Pt; intros; simpl. destruct (le_gt_dec j x); simpl. destruct (le_gt_dec k (x + (i + 1))); simpl. assert (x + i = pred (x + (i + 1))). lia. try_solve. lia. destruct (le_gt_dec k x); trivial. lia. trivial. rewrite (IHPt i (S j) (S k)); solve [trivial | lia]. rewrite (IHPt1 i j k); try lia. rewrite (IHPt2 i j k); try lia. trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)