(x y : Pos) {struct y} : BinInt := match x, y with | p~1, q~1 => binint_double ( p q) | p~1, q~0 => binint_succ_double ( p q) | p~1, 1 => pos p~0 | p~0, q~1 => binint_pred_double ( p q) | p~0, q~0 => binint_double ( p q) | p~0, 1 => pos (pos_pred_double p) | 1, q~1 => neg q~0 | 1, q~0 => neg (pos_pred_double q) | 1, 1 => zero end%pos.
Require Import Basics. Require Import Spaces.Pos.Core.