proposition: Lemma step_productive_h_S_inv_2: forall n (mu:Matrix)(alpha:Reals) (h:emits_h mu alpha),step_productive_h (S n) mu alpha -> step_productive_h n (fstT (sndT (modulus_h mu alpha h))) (sndT (sndT (modulus_h mu alpha h))).
proof: Proof. exact( fun (n : nat) (mu : Matrix) (alpha : Reals) (h : emits_h mu alpha) (H : step_productive_h (S n) mu alpha) => let H0 := match H in (step_productive_h n0 m r) return (n0 = S n -> m = mu -> r = alpha -> step_productive_h n (fstT (sndT (modulus_h mu alpha h))) (sndT (sndT (modulus_h mu alpha h)))) with | step_productive_h_O mu0 alpha0 H0 => fun (H1 : 0 = S n) (H2 : mu0 = mu) (H3 : alpha0 = alpha) => let H := (let H0 := eq_ind 0 (fun e : nat => match e with | O => True | S _ => False end) I (S n) H1 in False_ind (mu0 = mu -> alpha0 = alpha -> emits_h mu0 alpha0 -> step_productive_h n (fstT (sndT (modulus_h mu alpha h))) (sndT (sndT (modulus_h mu alpha h)))) H0) H2 H3 in H H0 | step_productive_h_S n0 mu0 alpha0 h0 H0 => fun (H1 : S n0 = S n) (H2 : mu0 = mu) (H3 : alpha0 = alpha) => let H := (let H0 := f_equal (fun e : nat => match e with | O => n0 | S n => n end) H1 in eq_ind n (fun n0 : nat => mu0 = mu -> alpha0 = alpha -> step_productive_h n0 (fstT (sndT (modulus_h mu0 alpha0 h0))) (sndT (sndT (modulus_h mu0 alpha0 h0))) -> step_productive_h n (fstT (sndT (modulus_h mu alpha h))) (sndT (sndT (modulus_h mu alpha h)))) (fun H2 : mu0 = mu => let H := eq_ind mu (fun m : Matrix => forall h0 : emits_h m alpha0, alpha0 = alpha -> step_productive_h n (fstT (sndT (modulus_h m alpha0 h0))) (sndT (sndT (modulus_h m alpha0 h0))) -> step_productive_h n (fstT (sndT (modulus_h mu alpha h))) (sndT (sndT (modulus_h mu alpha h)))) (fun (h0 : emits_h mu alpha0) (H3 : alpha0 = alpha) (H1 : step_productive_h n (fstT (sndT (modulus_h mu alpha0 h0))) (sndT (sndT (modulus_h mu alpha0 h0)))) => (let H := eq_ind_r (fun alpha0 : Reals => forall h0 : emits_h mu alpha0, step_productive_h n (fstT (sndT (modulus_h mu alpha0 h0))) (sndT (sndT (modulus_h mu alpha0 h0))) -> step_productive_h n (fstT (sndT (modulus_h mu alpha h))) (sndT (sndT (modulus_h mu alpha h)))) (fun h0 : emits_h mu alpha => eq_ind_r (fun p : prodT Digit (prodT Matrix Reals) => step_productive_h n (fstT (sndT (modulus_h mu alpha h0))) (sndT (sndT (modulus_h mu alpha h0))) -> step_productive_h n (fstT (sndT p)) (sndT (sndT p))) (fun H1 : step_productive_h n (fstT (sndT (modulus_h mu alpha h0))) (sndT (sndT (modulus_h mu alpha h0))) => H1) (modulus_h_PI mu alpha h h0)) H3 in H h0) H1) mu0 (sym_eq H2) in H h0) n0 (sym_eq H0)) H2 H3 in H H0 end in H0 (refl_equal (S n)) (refl_equal mu) (refl_equal alpha) ). Defined.
imports: digits