fact: Definition land (x y : zn2z t) := match x, y with | W0, _ => W0 | _, W0 => W0 | WW hx lx, WW hy ly => WW (ZnZ.land hx hy) (ZnZ.land lx ly) end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleAdd DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv CyclicAxioms