proposition: Lemma sub_mask_succ_r p q : sub_mask p (succ q) = sub_mask_carry p q.
proof: Proof. revert q. induction p as [p ?|p ?|]; intro q; destruct q; simpl; f_equal; trivial; now destruct p. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef