proposition: Lemma dicho_ext : forall (R : comRingType) (a b : R) n f1 f2 p, (p <= n)%N -> (forall i, (i <= n)%N -> f1 i = f2 i) -> dicho a b n f1 p = dicho a b n f2 p.
proof: Proof. move=> R a b n f1 f2 p pn q; rewrite /dicho; apply: ext_dc => i ci1 ci2. by apply/q/(leq_trans ci2); rewrite subnKC. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype order) mathcomp(div finfun bigop prime binomial ssralg finset fingroup finalg) mathcomp(mxalgebra perm zmodp matrix ssrint) mathcomp(seq rat) pol square_free casteljau desc mathcomp(ssrnum ssrint realalg poly) poly_normal