proposition: Theorem sub_mask_spec p q : SubMaskSpec p q (sub_mask p q).
proof: Proof. revert q. induction p as [p IHp|p IHp|]; intro q; destruct q as [q|q|]; simpl; try constructor; trivial. - destruct (IHp q) as [|r|r]; subst; try now constructor. now apply SubIsNeg with r~0. - destruct (IHp q) as [|r|r]; subst; try now constructor. apply SubIsNeg with (pred_double r). symmetry. apply add_xI_pred_double. - rewrite sub_mask_carry_spec. destruct (IHp q) as [|r|r]; subst; try constructor. + now apply SubIsNeg with 1. + destruct r; simpl; try constructor; simpl. * now rewrite add_carry_spec, <- add_succ_r. * now rewrite add_carry_spec, <- add_succ_r, succ_pred_double. * now rewrite add_1_r. + now apply SubIsNeg with r~1. - destruct (IHp q) as [|r|r]; subst; try now constructor. now apply SubIsNeg with r~0. - now rewrite add_1_l, succ_pred_double. - now apply SubIsNeg with q~0. - apply SubIsNeg with (pred_double q). now rewrite add_1_l, succ_pred_double. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef