proposition: Theorem inject_mult_fin_r (alpha : T1) : nf alpha -> forall n:nat, inject (alpha * n)%t1 = inject alpha * n.
proof: Proof. induction n. - simpl. destruct alpha; simpl; auto. destruct alpha1; simpl; auto. - destruct n. + simpl (inject alpha * 1). simpl (alpha * 1)%t1. destruct alpha; auto. destruct alpha1. * f_equal; destruct n; simpl; auto. assert (alpha2 = T1.zero). { eapply nf_of_finite; eauto. } -- subst. f_equal; ring. -- assert (alpha2 = T1.zero). { eapply nf_of_finite; eauto. } subst. replace (n * 1)%nat with n; auto with arith. * replace (n * 1)%nat with n; auto with arith. + change ((S (S n)):T1) with (FS (S n)); rewrite mult_Sn_add. replace (S (S n)) with (S (S (n + 0)))%nat. simpl mult_fin_r; rewrite inject_plus; auto with arith. * replace (alpha * (FS n))%t1 with (alpha * (S n))%t1. -- rewrite IHn; replace (n+0)%nat with n. reflexivity. auto with arith. -- reflexivity. * { clear IHn; induction n; simpl. destruct alpha; auto. destruct alpha1. apply nf_of_finite in H; subst; apply nf_FS. replace (n * 1)%nat with n; auto with arith. destruct alpha; auto with T1. destruct alpha1. apply nf_of_finite in H; subst; apply nf_FS. eapply nf_coeff_irrelevance. eauto. } * auto with arith. * auto. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)