Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- binom-identity : (a b : ℕ) -> (a + b) * (a + b) ≡ (a * a) + (b * b) + (2 * a * b)
- binom-identity zero b = sym (+-identityʳ (b * b))
- binom-identity (suc a) b = begin
- (1 + a + b) * (1 + a + b) ≡⟨⟩
- 1 + a + b + (a + b) * (1 + a + b) ≡⟨ cong (1 + a + b +_) (*-suc (a + b) (a + b)) ⟩
- 1 + (a + b) + ((a + b) + ((a + b) * (a + b))) ≡⟨ cong suc (sym (+-assoc (a + b) (a + b) ((a + b) * (a + b)))) ⟩
- 1 + (a + b) + (a + b) + (a + b) * (a + b) ≡⟨ cong suc (cong (_+ ((a + b) * (a + b))) (+-double-comm a b)) ⟩
- 1 + (a + a) + (b + b) + (a + b) * (a + b) ≡⟨ cong (1 + (a + a) + (b + b) +_) (binom-identity a b) ⟩
- 1 + (a + a) + (b + b) + (a * a + b * b + 2 * a * b) ≡⟨ cong (1 + (a + a) + (b + b) +_) (+-assoc (a * a) (b * b) (2 * a * b)) ⟩
- 1 + (a + a) + (b + b) + (a * a + (b * b + 2 * a * b)) ≡⟨ cong suc (sym (+-assoc (a + a + (b + b)) (a * a) (b * b + 2 * a * b))) ⟩
- 1 + (((a + a) + (b + b)) + (a * a)) + (b * b + 2 * a * b) ≡⟨ cong suc (cong (_+ (b * b + 2 * a * b)) {!!}) ⟩
- 1 + (((a + a) + a * a) + (b + b)) + (b * b + 2 * a * b) ≡⟨⟩
- {!!}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement