proposition: Lemma sub_mask_pos p q : q < p -> exists r, sub_mask p q = IsPos r.
proof: Proof. intros H. destruct (sub_mask_pos' p q H) as (r & Hr & _). now exists r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef