fact: Fixpoint lxor (p q:positive) : N := match p, q with | 1, 1 => N0 | 1, q~0 => Npos (q~1) | 1, q~1 => Npos (q~0) | p~0, 1 => Npos (p~1) | p~0, q~0 => Ndouble (lxor p q) | p~0, q~1 => Nsucc_double (lxor p q) | p~1, 1 => Npos (p~0) | p~1, q~0 => Nsucc_double (lxor p q) | p~1, q~1 => Ndouble (lxor p q) end.
imports: BinNums