ci/test1.v


1
2
3
4
5
6
7
8
9
10
11
12

Definition trois := 3. 
Print trois.
Eval compute in 10 * trois * trois.


Lemma  easy_proof : (forall A : Prop, A -> A). 
Proof using .
  intros A.
  intros proof_of_A.
  exact proof_of_A.
Qed.