Examples

Here are two examples:

def injective f = /\x,y (f x = f y -> x = y).

prop exo1 
  /\h,g (injective h & injective g &  /\x (h x = x or g x = x) 
      -> /\x (h (g x)) = (g (h x))).

let h, g assume injective h [H] and injective g [G] 
              and /\x (h x = x or g x = x) [C] 
  let x show h (g x) = g (h x).
by C with x assume h x = x then assume g x = x.
(* cas h x = x *)  
  by C with g x assume h (g x) = g x trivial 
           then assume g (g x) = g x [Eq].
  by G with Eq deduce g x = x trivial.
(* cas g x = x *)
  by C with h x assume g (h x) = h x trivial 
           then assume h (h x) = h x [Eq].
  by H with Eq deduce h x = x trivial.
save.

def inverse f A = \x (A (f x)).

def ouvert O = /\ x (O x -> \/a > R0 /\y (d x y < a -> O y)).

def continue1 f = /\ x  /\e > R0 \/a > R0
  /\ y (d x y < a -> d (f x) (f y) < e).

def continue2 f = /\ U ((ouvert U) -> (ouvert (inverse f U))).

goal /\f (continue1 f -> continue2 f).
let f assume continue1 f [F]
  let U assume ouvert U [O] show ouvert (inverse f U).
let x assume U (f x) [I] show \/b > R0  /\x' (d x x' < b -> U (f x')).
by O with f x let a assume a > R0 [i] and /\y (d (f x) y < a -> U y) [ii].
by F with x and i let b assume b > R0 [iii] and /\ x' (d x x' < b -> d (f x) (f x') < a) [iv].
let x' assume d x x' < b [v] show U (f x').
by ii with f x' show d (f x) (f x') < a.
by iv with v trivial.
save th1.