proposition: Lemma E0_canon_lt (a: E0) i: cnf a <> zero -> E0lt (E0Canon a i) a.
proof: Proof. move: i; case : a => cnf Heq i Hpos; rewrite /E0Canon /E0lt => /=. pattern cnf at 2; rewrite -(h2g_g2hK cnf) -hlt_iff h2g_g2hK; apply Canon.canon_lt. - rewrite hnf_g2h; by apply /eqP. - rewrite /Hpos -h2g_eqE h2g_g2hK => H0; apply Hpos; subst; by rewrite -g2h_eqE. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)