proposition: Lemma L_phi0_mult_ok i: L_spec (T1.cons alpha i zero) (L_phi0_mult (S i)).
proof: Proof. induction i. - unfold L_phi0_mult; simpl. assumption. - unfold L_phi0_mult. + right. * discriminate. * intro k; red; path_decompose (Nat.pred (f (S k))). instantiate (1:= (T1.cons alpha i zero)). -- rewrite iterate_rw; inversion_clear IHi. specialize (H0 (Nat.pred (f (S k)))). rewrite S_pred_rw in *; auto. -- apply path_to_mult; auto; apply f_ok_inv. -- generalize (f_Sle (S k)); abstract lia. -- generalize (iterate_Sge f i f_Sle (f (S k))); intro; rewrite iterate_rw; abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)