proposition: Lemma chfun_3 : forall k j a, (forall i, 1 <= k i /\ k i <= n) -> 1 <= a -> a <= n -> forall i, 1 <= chfun k a j i /\ chfun k a j i <= n.
proof: Proof. intros. unfold chfun in |- *. elim (le_gt_dec i j). auto. auto. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)