proposition: Lemma sub_xO_xI n m : n~0 - m~1 = pred_double (n-m).
proof: Proof. unfold sub. simpl. rewrite sub_mask_carry_spec. now destruct (sub_mask n m) as [|[r|r|]|]. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef