proposition: Lemma Least_is_0 (alpha:t) : Least alpha <-> alpha = 0.
proof: Proof. unfold Least; split; intro H. - destruct alpha. + destruct n. * reflexivity. * specialize (H (inl n)); inversion H. -- inversion H0; abstract lia. -- abstract lia. + specialize (H (inl 0)); inversion H. * inversion H0. - subst; destruct y. + destruct n. * right. * left; constructor. abstract lia. + constructor. constructor. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)