proposition: Lemma sub_le p q : p<=q -> p-q = 1.
proof: Proof. unfold le, sub. rewrite compare_sub_mask. destruct sub_mask; easy'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef