fact: Definition independence (i j : 'I_n) := ~~ closure parent [set i] j -> let parents := [set k | closure parent [set k] i] in cinde_preim [set i] [set j] parents.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba