proposition: Theorem sub_mask_nul_iff p q : sub_mask p q = IsNul <-> p = q.
proof: Proof. split. - now case sub_mask_spec. - intros <-. induction p as [p IHp|p IHp|]; simpl; now rewrite ?IHp. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef