Require Import ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* 1/ Find in the library a theorem that expresses that when a prime number
   divides a product of two factors, then it divides one of the factors. 
   What modules do you think should be loaded (using Require Import ...)?
   How can you use the Search command, so that it returns exactly this
   theorem? *)

(* 2/ What is behind the notation "_ < _" for natural numbers? What is the theorem
   that expresses that if you have "x.+1 <= y.+1" then you also have "x <= y". *)

(* 3/ Find the definition for the notion "cancel". Find theorems relying on this
   notion. What do they have in common? What are the theorems expressing the
   relation between addition and subtraction? *)



Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.