fact: Fixpoint get_pair x := match x with | xI (xO p) => (xH,p) | xO (xO x) => let '(x,y) := get_pair x in (xO x,y) | xI (xI x) => let '(x,y) := get_pair x in (xI x,y) | _ => assert_false (xH,xH) end.
imports: common positives ordinal