proposition: Lemma prelift_aux_fold : forall Pt m n i, prelift_aux (m + n) Pt i = prelift_aux m (prelift_aux n Pt i) i.
proof: Proof. intros. rewrite prelift_aux_fold_aux; try_solve. lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)