proposition: Lemma l_std_ok : forall alpha : E0, alpha != E0zero -> forall k : nat, (1 <= k)%N -> battle_length standard k (T1toH (cnf alpha)) (l_std alpha k).
proof: Proof. move => alpha Halpha k /leP Hk; rewrite /l_std. have H0: E0_g2h alpha <> hE0zero by rewrite -g2h_E0zero; apply /E0_diffE /diffP. move: (Battle_length.l_std_ok (E0_g2h alpha) H0 k Hk); rewrite /L_ => He; by apply He. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg Hydra_Theorems Hydra_Definitions Hydra_Termination Battle_length Hydra_Examples Epsilon0_Needed_Free Epsilon0_Needed_Std) T1Bridge GHessenberg GL_alpha GPrelude