proposition: Lemma chfun_2 : forall k j a i, j < i -> a = chfun k a j i.
proof: Proof. intros. unfold chfun in |- *. elim (le_gt_dec i j). intro y. elim (proj1 (Nat.le_ngt _ _) y H). auto. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)