Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Rbase. Require Import Rfunctions. Require Import PartSum. Local Open Scope R_scope. Definition C (n p:nat) : R := INR (fact n) / (INR (fact p) * INR (fact (n - p))).forall n i : nat, (i <= n)%nat -> C n i = C n (n - i)forall n i : nat, (i <= n)%nat -> C n i = C n (n - i)n, i:natH:(i <= n)%natINR (fact n) / (INR (fact i) * INR (fact (n - i))) = INR (fact n) / (INR (fact (n - i)) * INR (fact i))n, i:natH:(i <= n)%nati = (n - (n - i))%natn, i:natH:(i <= n)%natINR (fact n) / (INR (fact (n - i)) * INR (fact i)) = INR (fact n) / (INR (fact (n - i)) * INR (fact i))n, i:natH:(i <= n)%nati = (n - (n - i))%natapply plus_minus; rewrite plus_comm; apply le_plus_minus; assumption. Qed.n, i:natH:(i <= n)%nati = (n - (n - i))%natforall n i : nat, (i <= n)%nat -> C (S n) i = INR (S n) / INR (S n - i) * C n iforall n i : nat, (i <= n)%nat -> C (S n) i = INR (S n) / INR (S n - i) * C n in, i:natH:(i <= n)%natINR (fact (S n)) / (INR (fact i) * INR (fact (S (n - i)))) = INR (S n) / INR (S (n - i)) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%nat(forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat) -> INR (fact (S n)) / (INR (fact i) * INR (fact (S (n - i)))) = INR (S n) / INR (S (n - i)) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S n * fact n) / (INR (fact i) * INR (S (n - i) * fact (n - i))) = INR (S n) / INR (S (n - i)) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S n) * INR (fact n) * (/ INR (fact i) * (/ INR (S (n - i)) * / INR (fact (n - i)))) = INR (S n) * / INR (S (n - i)) * (INR (fact n) * (/ INR (fact i) * / INR (fact (n - i))))n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) * INR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) * INR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) * INR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) * INR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) * INR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact i) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) * INR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) * INR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (S (n - i)) <> 0n, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact (n - i)) <> 0n, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natn, i:natH:(i <= n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i <= n)%natS (n - i) = (S n - i)%natapply minus_Sn_m; assumption. Qed.n, i:natH:(i <= n)%natS (n - i) = (S n - i)%natforall n i : nat, (i < n)%nat -> C n (S i) = INR (n - i) / INR (S i) * C n iforall n i : nat, (i < n)%nat -> C n (S i) = INR (n - i) / INR (S i) * C n in, i:natH:(i < n)%natINR (fact n) / (INR (fact (S i)) * INR (fact (n - S i))) = INR (n - i) / INR (S i) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i < n)%nat(forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat) -> INR (fact n) / (INR (fact (S i)) * INR (fact (n - S i))) = INR (n - i) / INR (S i) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natINR (fact n) / (INR (fact (S i)) * INR (fact (n - S i))) = INR (n - i) / INR (S i) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i) -> INR (fact n) / (INR (fact (S i)) * INR (fact (n - S i))) = INR (n - i) / INR (S i) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact n) / (INR (fact (S i)) * INR (fact (n - S i))) = INR (n - i) / INR (S i) * (INR (fact n) / (INR (fact i) * INR (fact (n - i))))n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact n) / (INR (fact (S i)) * INR (fact (n - S i))) = INR (n - i) / INR (S i) * (INR (fact n) / (INR (fact i) * INR (fact (S (n - S i)))))n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact n) * (/ INR (S i) * / INR (fact i) * / INR (fact (n - S i))) = INR (n - i) * / INR (S i) * (INR (fact n) * (/ INR (fact i) * (/ INR (S (n - S i)) * / INR (fact (n - S i)))))n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) * INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact n) * (/ INR (S i) * (/ INR (fact i) * / INR (fact (n - S i)))) = / INR (S i) * (INR (fact n) * (/ INR (fact i) * (/ INR (fact (n - S i)) * 1)))n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (n - i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) * INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (n - i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) * INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) * INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) * INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) * INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S (n - S i)) * INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (S i) * INR (fact i) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%natH1:(n - i)%nat = S (n - S i)INR (fact (n - S i)) <> 0n, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = S (n - S i)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(n - i)%nat = (S n - S i)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(S i <= n)%natn, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natn, i:natH:(i < n)%natH0:forall n0 : nat, fact (S n0) = (S n0 * fact n0)%nat(S i <= n)%natn, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natintro; reflexivity. Qed. (**********)n, i:natH:(i < n)%natforall n0 : nat, fact (S n0) = (S n0 * fact n0)%natforall n i : nat, (i < n)%nat -> C n i + C n (S i) = C (S n) (S i)forall n i : nat, (i < n)%nat -> C n i + C n (S i) = C (S n) (S i)n, i:natH:(i < n)%natC n i + C n (S i) = C (S n) (S i)n, i:natH:(i < n)%natC n i + INR (n - i) / INR (S i) * C n i = C (S n) (S i)n, i:natH:(i < n)%natC n i * (1 + INR (n - i) / INR (S i)) = C (S n) (S i)n, i:natH:(i < n)%natC n i * (INR (S n) / INR (S i)) = C (S n) (S i)n, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natC n (n - i) * (INR (S n) / INR (S i)) = C (S n) (S i)n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natINR (S n) / INR (S n - (n - i)) * C n (n - i) = C (S n) (S n - (n - i))n, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natC (S n) (n - i) = C (S n) (S n - (n - i))n, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(n - i <= S n)%natn, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(n <= S n)%natn, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%nat(n <= S n)%natn, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(n <= S n)%natn, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(S n - (n - i))%nat = S in, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natS (n - (n - i)) = S in, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(n - (n - i))%nat = i -> S (n - (n - i)) = S in, i:natH:(i < n)%nat(n - (n - i))%nat = in, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(n - (n - i))%nat = in, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natn = (n - i + i)%natn, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natn = nn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(n - i <= n)%natn, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natINR (S n) / INR (S i) = 1 + INR (n - i) / INR (S i)n, i:natH:(i < n)%natINR (S n) * / INR (S i) = 1 + INR (n - i) * / INR (S i)n, i:natH:(i < n)%nat(INR n + 1) * / (INR i + 1) = 1 + INR (n - i) * / (INR i + 1)n, i:natH:(i < n)%nat(INR n + 1) * / (INR i + 1) = 1 + (INR n - INR i) * / (INR i + 1)n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR i + 1 <> 0 -> (INR n + 1) * / (INR i + 1) = 1 + (INR n - INR i) * / (INR i + 1)n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natH0:INR i + 1 <> 0(INR n + 1) * / (INR i + 1) = 1 + (INR n - INR i) * / (INR i + 1)n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natH0:INR i + 1 <> 0(INR i + 1) * ((INR n + 1) * / (INR i + 1)) = (INR i + 1) * (1 + (INR n - INR i) * / (INR i + 1))n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natH0:INR i + 1 <> 0(INR i + 1) * ((INR n + 1) * / (INR i + 1)) = (INR i + 1) * 1 + (INR i + 1) * ((INR n - INR i) * / (INR i + 1))n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natH0:INR i + 1 <> 0(INR i + 1) * ((INR n + 1) * / (INR i + 1)) = INR i + 1 + (INR i + 1) * ((INR n - INR i) * / (INR i + 1))n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natH0:INR i + 1 <> 0(INR n + 1) * / (INR i + 1) * (INR i + 1) = INR i + 1 + (INR n - INR i) * / (INR i + 1) * (INR i + 1)n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natH0:INR i + 1 <> 0(INR n + 1) * (/ (INR i + 1) * (INR i + 1)) = INR i + 1 + (INR n - INR i) * (/ (INR i + 1) * (INR i + 1))n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natH0:INR i + 1 <> 0(INR n + 1) * 1 = INR i + 1 + (INR n - INR i) * 1n, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR i + 1 <> 0n, i:natH:(i < n)%nat(i <= n)%natn, i:natH:(i < n)%natINR (S i) <> 0n, i:natH:(i < n)%nat(i <= n)%natapply lt_le_weak; assumption. Qed. (*********************) (*********************)n, i:natH:(i < n)%nat(i <= n)%natforall (x y : R) (n : nat), (x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall (x y : R) (n : nat), (x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nx, y:R(x + y) ^ 0 = sum_f_R0 (fun i : nat => C 0 i * x ^ i * y ^ (0 - i)) 0x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n(x + y) ^ (n + 1) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nsum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) ^ 1 = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nsum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nsum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + C (S n) (S n) * x ^ S n * y ^ (S n - S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n(forall p : nat, C p p = 1) -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + C (S n) (S n) * x ^ S n * y ^ (S n - S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n(forall p : nat, C p 0 = 1) -> (forall p : nat, C p p = 1) -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + C (S n) (S n) * x ^ S n * y ^ (S n - S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nH:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S n * y ^ 0x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nH:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:RHrecn:(x + y) ^ 0 = sum_f_R0 (fun i : nat => C 0 i * x ^ i * y ^ (0 - i)) 0H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1sum_f_R0 (fun i : nat => C 0 i * x ^ i * y ^ (0 - i)) 0 * (x + y) = sum_f_R0 (fun i : nat => C 1 i * x ^ i * y ^ (1 - i)) 0 + x ^ 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nsum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n) * (x + y) = sum_f_R0 (fun i : nat => C (S (S n)) i * x ^ i * y ^ (S (S n) - i)) (S n) + x ^ S (S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1(* N >= 1 *)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nsum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n) * (x + y) = sum_f_R0 (fun i : nat => C (S (S n)) i * x ^ i * y ^ (S (S n) - i)) (S n) + x ^ S (S n)x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * (x + y) = sum_f_R0 (fun i : nat => C (S N) i * x ^ i * y ^ (S N - i)) N + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * x + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * y = sum_f_R0 (fun i : nat => C (S N) i * x ^ i * y ^ (S N - i)) N + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * y = sum_f_R0 (fun i : nat => C (S N) i * x ^ i * y ^ (S N - i)) N + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C (S N) i * x ^ i * y ^ (S N - i)) N + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = C (S N) 0 * x ^ 0 * y ^ (S N - 0) + sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) (Init.Nat.pred N) + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = 1 * 1 * y ^ (S N - 0) + sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) (Init.Nat.pred N) + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ (S N - 0) + sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) (Init.Nat.pred N) + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) (Init.Nat.pred N) + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) (Init.Nat.pred N) + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) (Init.Nat.pred N) + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) n + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + sum_f_R0 (fun i : nat => An i + Bn i) n + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + (sum_f_R0 An n + sum_f_R0 Bn n) + x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + (sum_f_R0 An n + sum_f_R0 Bn n) + An (S n)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + (sum_f_R0 Bn n + sum_f_R0 An n) + An (S n)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + (sum_f_R0 Bn n + (sum_f_R0 An n + An (S n)))x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + (sum_f_R0 Bn n + sum_f_R0 An (S n))x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 An N + sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = y ^ S N + (sum_f_R0 Bn n + sum_f_R0 An N)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rsum_f_R0 An N + sum_f_R0 Cn N = y ^ S N + (sum_f_R0 Bn n + sum_f_R0 An N)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> R(forall i : nat, (i < N)%nat -> Cn (S i) = Bn i) -> sum_f_R0 An N + sum_f_R0 Cn N = y ^ S N + (sum_f_R0 Bn n + sum_f_R0 An N)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 An N + sum_f_R0 Cn N = y ^ S N + (sum_f_R0 (fun i : nat => Cn (S i)) n + sum_f_R0 An N)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 An N + sum_f_R0 Cn N = Cn 0%nat + (sum_f_R0 (fun i : nat => Cn (S i)) n + sum_f_R0 An N)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn iCn 0%nat = y ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 An N + (Cn 0%nat + sum_f_R0 (fun i : nat => Cn (S i)) (Init.Nat.pred N)) = Cn 0%nat + sum_f_R0 (fun i : nat => Cn (S i)) n + sum_f_R0 An Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn i(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn iCn 0%nat = y ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 An N + (Cn 0%nat + sum_f_R0 (fun i : nat => Cn (S i)) n) = Cn 0%nat + sum_f_R0 (fun i : nat => Cn (S i)) n + sum_f_R0 An Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn in = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn i(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn iCn 0%nat = y ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn in = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn i(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn iCn 0%nat = y ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn i(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn iCn 0%nat = y ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn iCn 0%nat = y ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn isum_f_R0 (fun i : nat => Cn (S i)) n = sum_f_R0 Bn nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> RH1:forall i : nat, (i < N)%nat -> Cn (S i) = Bn iforall i : nat, (i <= n)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:natAn:=fun i0 : nat => C N i0 * x ^ S i0 * y ^ (N - i0):nat -> RBn:=fun i0 : nat => C N (S i0) * x ^ S i0 * y ^ (N - i0):nat -> RCn:=fun i0 : nat => C N i0 * x ^ i0 * y ^ (S N - i0):nat -> RH1:forall i0 : nat, (i0 < N)%nat -> Cn (S i0) = Bn i0i:natH2:(i <= n)%nat(i < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RCn:=fun i : nat => C N i * x ^ i * y ^ (S N - i):nat -> Rforall i : nat, (i < N)%nat -> Cn (S i) = Bn ix, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> RAn (S n) = x ^ S Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rsum_f_R0 (fun i : nat => An i + Bn i) n = sum_f_R0 (fun i : nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rforall i : nat, (i <= n)%nat -> An i + Bn i = C (S N) (S i) * x ^ S i * y ^ (S N - S i)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:natAn:=fun i0 : nat => C N i0 * x ^ S i0 * y ^ (N - i0):nat -> RBn:=fun i0 : nat => C N (S i0) * x ^ S i0 * y ^ (N - i0):nat -> Ri:natH1:(i <= n)%natC N i * x ^ S i * y ^ (N - i) + C N (S i) * x ^ S i * y ^ (N - i) = C (S N) (S i) * x ^ S i * y ^ (S N - S i)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:natAn:=fun i0 : nat => C N i0 * x ^ S i0 * y ^ (N - i0):nat -> RBn:=fun i0 : nat => C N (S i0) * x ^ S i0 * y ^ (N - i0):nat -> Ri:natH1:(i <= n)%natC N i * x ^ S i * y ^ (N - i) + C N (S i) * x ^ S i * y ^ (N - i) = C (S N) (S i) * x ^ S i * y ^ (N - i)x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natAn:=fun i : nat => C N i * x ^ S i * y ^ (N - i):nat -> RBn:=fun i : nat => C N (S i) * x ^ S i * y ^ (N - i):nat -> Rn = Init.Nat.pred Nx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:nat(0 < N)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (S N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natforall i : nat, (i <= N)%nat -> C N i * x ^ i * y ^ (S N - i) = C N i * x ^ i * y ^ (N - i) * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:nati:natH1:(i <= N)%natC N i * x ^ i * y ^ S (N - i) = C N i * x ^ i * y ^ (N - i) * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:nati:natH1:(i <= N)%natS (N - i) = (S N - i)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:nati:natH1:(i <= N)%natC N i * x ^ i * y ^ (N - i + 1) = C N i * x ^ i * y ^ (N - i) * yx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:nati:natH1:(i <= N)%natS (N - i) = (S N - i)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n -> sum_f_R0 (fun i0 : nat => C n i0 * x ^ i0 * y ^ (n - i0)) n * (x + y) = sum_f_R0 (fun i0 : nat => C (S n) i0 * x ^ i0 * y ^ (S n - i0)) n + x ^ S nN:=S n:nati:natH1:(i <= N)%natS (N - i) = (S N - i)%natx, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natsum_f_R0 (fun i : nat => C N i * x ^ S i * y ^ (N - i)) N = sum_f_R0 (fun i : nat => C N i * x ^ i * y ^ (N - i)) N * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ S n = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) (S n)H:forall p : nat, C p 0 = 1H0:forall p : nat, C p p = 1Hrecn0:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n -> sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) n * (x + y) = sum_f_R0 (fun i : nat => C (S n) i * x ^ i * y ^ (S n - i)) n + x ^ S nN:=S n:natforall i : nat, (i <= N)%nat -> C N i * x ^ S i * y ^ (N - i) = C N i * x ^ i * y ^ (N - i) * xx, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p 0 = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) np:natINR (fact p) / (INR (fact 0) * INR (fact (p - 0))) = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) np:natINR (fact p) / (1 * INR (fact (p - 0))) = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) np:natINR (fact p) / (1 * INR (fact p)) = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) nforall p : nat, C p p = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) np:natINR (fact p) / (INR (fact p) * INR (fact (p - p))) = 1x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) np:natINR (fact p) / (INR (fact p) * INR (fact 0)) = 1rewrite Rmult_1_r; unfold Rdiv; rewrite <- Rinv_r_sym; [ reflexivity | apply INR_fact_neq_0 ]. Qed.x, y:Rn:natHrecn:(x + y) ^ n = sum_f_R0 (fun i : nat => C n i * x ^ i * y ^ (n - i)) np:natINR (fact p) / (INR (fact p) * 1) = 1