proposition: Lemma mult_Sn_dist (alpha : Ord) (n p : nat) : mult_Sn alpha (S (n + p)) = mult_Sn alpha p + mult_Sn alpha n.
proof: Proof. induction n; simpl. - reflexivity. - rewrite plus_assoc; f_equal. now rewrite <- IHn. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)