proposition: Lemma pos_ldiff_spec p p' n : testbit (Pos.ldiff p p') n = (Pos.testbit p n) && negb (Pos.testbit p' n).
proof: Proof. revert p' n. induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl; (specialize (IH p'); destruct Pos.ldiff; trivial; now rewrite <-IH) || (now rewrite andb_true_r). Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties