proposition: Lemma compare_sub_mask p q : (p ?= q) = mask2cmp (sub_mask p q).
proof: Proof. revert q. induction p as [p IHp| p IHp| ]; intros [q|q| ]; simpl; trivial; specialize (IHp q); rewrite ?sub_mask_carry_spec; destruct (sub_mask p q) as [|r|]; simpl in *; try clear r; try destruct r; simpl; trivial; simpl_compare; now rewrite IHp. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef