proposition: Lemma sub_mask_pos' p q : q < p -> exists r, sub_mask p q = IsPos r /\ q + r = p.
proof: Proof. rewrite lt_iff_add. intros (r,Hr). exists r. split; trivial. now apply sub_mask_pos_iff. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef