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