proposition: Lemma sub_mask_add_diag_r p q : sub_mask p (p+q) = IsNeg.
proof: Proof. case sub_mask_spec; trivial. - intros H. symmetry in H; rewrite add_comm in H. elim (add_no_neutral _ _ H). - intros r H. rewrite <- add_assoc, add_comm in H. elim (add_no_neutral _ _ H). Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef