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