COQ in CoCalc

Require Import Coq.Logic.JMeq.

Inductive Le : nat -> nat -> Set :=
     | LeO : forall n:nat, Le 0 n
     | LeS : forall n m:nat, Le n m -> Le (S n) (S m).

Parameter P : nat -> nat -> Prop.

Goal forall n m:nat, Le (S n) m -> P n m.

intros n m H.

generalize_eqs H.

Theorem implication :
  forall A B : Prop,
  A ->
  (A -> B) ->
  B
.

Proof.
  intros A B.
  intros proof_of_A.
  intros A_implies_B.
  pose (proof_of_B := A_implies_B proof_of_A).
  exact proof_of_B.
Qed.

Theorem t3 : bool. Proof. pose (b1 := true). pose (b2 := false).

exact b2.

Compute
    match 0 with
      | 0 => 1 + 1
      | S n' => n'
    end.