proposition: Theorem sub_mask_diag p : sub_mask p p = IsNul.
proof: Proof. now apply sub_mask_nul_iff. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef