proposition: Lemma o_bool_ok : forall a1 a2, match o_bool a1 a2 with true => o a1 a2 | false => ~ o a1 a2 end.
proof: Proof. unfold o; fix o_bool_ok 1. intros [ | n] [ | m]; simpl. apply le_n. apply Nat.le_0_l. intro H; inversion H. generalize (o_bool_ok n m); case (o_bool n m). intro H; apply (le_n_S _ _ H). intros H H'; apply H; apply (le_S_n _ _ H'). Defined.
imports: Coq(Setoid Relations Arith FunInd)