proposition: Lemma sub_mask_add_diag_l p q : sub_mask (p+q) p = IsPos q.
proof: Proof. case sub_mask_spec. - intros H. rewrite add_comm in H. elim (add_no_neutral _ _ H). - intros r H. apply add_cancel_l in H. now f_equal. - 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