proposition: Lemma Pminus_mask_carry_spec : forall p q, Pminus_mask_carry p q = Pminus_mask p (Pos.succ q).
proof: Proof. intros p q;generalize q p;clear q p. induction q;destruct p;simpl;try rewrite IHq;trivial. destruct p;trivial. destruct p;trivial. Qed.
imports: ZArith Lia