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