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