fact: Fixpoint pos_plus (a b:pos) {struct a} : pos := match a with one => pos_succ b | xL x => match b with one => xR x | xL y => xL (pos_plus x y) | xR y => xR (pos_plus x y) end | xR x => match b with one => xL (pos_succ x) | xL y => xR (pos_plus x y) | xR y => xL (pos_succ (pos_plus x y)) end end.