proposition: Lemma gt_iff_add p q : p > q <-> exists r, q + r = p.
proof: Proof. unfold ">". rewrite compare_sub_mask. split. - case_eq (sub_mask p q); try discriminate; intros r Hr _. exists r. now apply sub_mask_pos_iff. - intros (r,Hr). apply sub_mask_pos_iff in Hr. now rewrite Hr. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef