fact: Fixpoint pos_ineq (a b:pos) {struct a}: ineq := match a, b with one, one => i_eq | one, _ => i_lt | xL u, one => i_gt | xL u, xL v => pos_ineq u v | xL u, xR v => match (pos_ineq u v) with i_gt => i_gt | i_eq => i_lt | i_lt => i_lt end| xR u, one => i_gt | xR u, xL v => match (pos_ineq u v) with i_gt => i_gt | i_eq => i_gt | i_lt => i_lt end | xR u, xR v => pos_ineq u v end.