proposition: Lemma chfun_4 : forall k j a, (forall i, k (S i) <= k i) -> a <= k j -> forall i, chfun k a j (S i) <= chfun k a j i.
proof: Proof. intros. unfold chfun in |- *. elim (le_gt_dec i j); elim (le_gt_dec (S i) j); intros; auto. cut (i = j). intro. rewrite H1. auto. lia. lia. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)