proposition: Theorem sub_add p q : q < p -> (p-q)+q = p.
proof: Proof. intros H. destruct (sub_mask_pos p q H) as (r,U). unfold sub. rewrite U. rewrite add_comm. now apply sub_mask_add. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef