fact: Definition base_two_reverse n := let F := the_expansion \2c n in let p := cardinal (domain F) in expansion_value (Lg p (fun z => (Vg F (p -c (csucc z))))) \2c.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)