fact: Fixpoint takes {k : nat} (w : k.-tuple A) (s : seq A) {struct s} : seq A := if s is _ :: t then let s' := takes w t in if take k s == w then nth def (drop k s) O :: s' else s' else [::].
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb fdist entropy convex ln_facts jensen num_occ