proposition: Lemma prelower_prelift : forall Pt i, prelift Pt i = prelower_aux (prelift Pt (i + 1)) i.
proof: Proof. intros; unfold prelift. apply prelower_prelift_aux. lia. lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)