fact: Fixpoint int_pos_sub (x y : Pos) {struct y} : Int := match x, y with | p~1, q~1 => int_double (int_pos_sub p q) | p~1, q~0 => int_succ_double (int_pos_sub p q) | p~1, 1 => pos p~0 | p~0, q~1 => int_pred_double (int_pos_sub p q) | p~0, q~0 => int_double (int_pos_sub 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.
imports: Basics Spaces.Pos.Core