proposition: Lemma L2 : beta = zero -> P beta.
proof: Proof. intro; subst; unfold P; rewrite mult_a_0. split; auto. intros H0 gamma H1; destruct (not_LT_zero H1). Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)