proposition: Lemma pos_lor_spec p p' n : Pos.testbit (Pos.lor p p') n = (Pos.testbit p n) || (Pos.testbit p' n).
proof: Proof. revert p' n. induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl; apply IH || now rewrite orb_false_r. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties