fact: Definition var_rec (a b : C.T) (n : nat) := C.mask (C.mask C.zero a) b.
imports: Coq(ZArith Reals) Flocq(Raux) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval Datatypes Basic_rec