proposition: Lemma compare_reflect alpha beta : match (ON_compare alpha beta) with Lt => alpha o< beta | Eq => alpha = beta | Gt => beta o< alpha end.
proof: Proof. destruct alpha, beta; cbn; unfold ON_compare. destruct (comparable_comp_spec (n,n0) (n1,n2)). - rewrite H, compare_refl; reflexivity. - apply compare_lt_iff in H. rewrite H. apply compare_lt_iff. assumption. - apply compare_gt_iff in H. rewrite H. apply compare_gt_iff. assumption. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)