proposition: Corollary Successor_not (i j k : nat) : ~ Successor (k,0) (i,j).
proof: Proof. intro H; apply Successor_inv in H. destruct H; discriminate. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)