Theorem example_1 : forall A B: Prop, ((A \/ B) /\ ~A) -> B.
Proof.
intros A B.
intros H.
elim H.
intros H_AorB.
intros H_notA.
elim H_AorB.

  intros H_A.
  elim H_notA.
  exact H_A.

  intros H_B.
  exact H_B.
Qed.




Require Import Arith.


Fixpoint sum_n (n:nat) : nat :=
    match n with 0 => 0
               | S p => S p + sum_n p
    end.

Theorem example_2 : forall n : nat, 2 * sum_n n = n * n + n.

intros n.
elim n.
simpl.
reflexivity.
intros k.
intros H.
simpl; ring_simplify.
rewrite H.
simpl; ring_simplify.
reflexivity.
Qed.





(*

Basecase (n = 0):
2 * 0 = 0 * 0 + 0
- ok

Hypothesis (n = k):
2 * (1 + 2 + ... + k) = k * k + k

Inductive step (n = k + 1):
2 * (1 + 2 + ... + k + k+1) = (k+1) * (k+1) + (k+1)
2 * (1 + 2 + ... + k) + 2 * (k+1) = (k+1) * (k+1) + (k+1)
k * k + k + 2 * (k+1) = k * k + k + k + 1 + k + 1
k * k + 3 * k + 2 = k * k + 3 * k + 2
- ok

*)