proposition: Lemma sub_xO_xO n m : m<n -> n~0 - m~0 = (n-m)~0.
proof: Proof. intros H. unfold sub. simpl. now destruct (sub_mask_pos n m H) as (p, ->). Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef