fact: Record Partition (a b : IR) (Hab : a [<=] b) (lng : nat) : Type := {Pts :> forall i, i <= lng -> IR; prf1 : forall i j, i = j -> forall Hi Hj, Pts i Hi [=] Pts j Hj; prf2 : forall i Hi HSi, Pts i Hi [<=] Pts (S i) HSi; start : forall H, Pts 0 H [=] a; finish : forall H, Pts lng H [=] b}.
imports: CoRN.ftc.Continuity Coq(Lia)