proposition: Lemma foldi_ge : forall A f from to (a:A), to <=? from = true -> foldi f from to a = a.
proof: Proof. intros A f from to a; unfold foldi. intro H; rewrite H; reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz