proposition: Lemma ldiff_spec a a' n : testbit (ldiff a a') n = (testbit a n) && negb (testbit a' n).
proof: Proof. destruct a, a'; simpl; trivial. - now rewrite andb_true_r. - apply pos_ldiff_spec. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties