proposition: Lemma PZero : P E0zero.
proof: Proof. split; auto with E0. - now destruct 1. - unfold Canon_plus ; intros. unfold E0zero in H; simpl in H. destruct n. + inversion H. + destruct (const_pathS_zero H). Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)