proposition: Lemma pos_sub_spec p q : pos_sub p q = match (p ?= q)%positive with | Eq => 0 | Lt => neg (q - p) | Gt => pos (p - q) end.
proof: Proof. revert q. induction p as [p IHp|p IHp|]; intros q; destruct q; simpl; trivial; rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xI_xO, ?Pos.compare_xO_xO, IHp; simpl; case Pos.compare_spec; intros; simpl; trivial; (now rewrite Pos.sub_xI_xI) || (now rewrite Pos.sub_xO_xO) || (now rewrite Pos.sub_xO_xI) || (now rewrite Pos.sub_xI_xO) || subst; unfold Pos.sub; simpl; now rewrite Pos.sub_mask_diag. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass