fact: Fixpoint lor (p q : positive) : positive := match p, q with | 1, q~0 => q~1 | 1, _ => q | p~0, 1 => p~1 | _, 1 => p | p~0, q~0 => (lor p q)~0 | p~0, q~1 => (lor p q)~1 | p~1, q~0 => (lor p q)~1 | p~1, q~1 => (lor p q)~1 end.
imports: BinNums