diff --git a/examples/math_exam/BAC2017.thy b/examples/math_exam/BAC2017.thy
index ddcde1a..cbae2cf 100644
--- a/examples/math_exam/BAC2017.thy
+++ b/examples/math_exam/BAC2017.thy
@@ -9,6 +9,10 @@ section*[idir::Author,affiliation="''CentraleSupelec''",
 email="''idir.aitsadoune@centralesupelec.fr''"]
 {*Idir AIT SADOUNE*}
 
+section*[keller::Author,affiliation="''LRI, Univ. Paris-Sud''", 
+email="''Chantal.Keller@lri.fr''"]
+{*Chantal KELLER*}
+
 subsection*[header::Header,examSubject= "[algebra,geometry]", 
  examTitle="''BACCALAUREAT GENERAL MATHEMATIQUES''", 
 date="''21-06-2017''", 
@@ -24,7 +28,7 @@ timeAllowed="240::int"]
 *}
 
 subsubsection*[exo1 :: Exercise,Exercise.concerns= "{examiner,validator,student}",
-Exercise.content="[q1::Task]"]
+Exercise.content="[q1::Task,q2,q3a]"]
 {* 
 On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par : @{term "h(x) = x * exponent (-x)"}
 *}
@@ -38,7 +42,7 @@ level="oneStar", mark="1::int", type="formal"]
 {* Déterminer la limite de la fonction @{term h} en +\<infinity>. *}
 
 text*[a1::Answer_Formal_Step]
-{* First Step: Fill in term and justification*}
+{* Fill in term and justification*}
 
 lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top"
   sorry
@@ -47,25 +51,50 @@ lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top"
 subsubsection*[q2::Task, Task.concerns= "{examiner,validator,student}",
 level="oneStar", mark="1::int", type="formal"] 
 {* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\<infinity>] et dresser son tableau
-   de variation} *}
-find_theorems exp
+   de variation *}
+
 
 text*[a2::Answer_Formal_Step]
-{* First Step: Fill in term and justification*}
+{* Fill in term and justification*}
 
-lemma q2_a : "DERIV h x :> (1 - x) * exp (- x)"
+
+definition h' :: "real \<Rightarrow> real"
+  where "h' x \<equiv> (1 - x) * exp (- x)"
+
+lemma q2_a : "DERIV h x :> h' x"
 proof -
   have * : "DERIV (exp \<circ> uminus) x :> - (exp (-x))"
-    by (simp add: has_derivative_minus has_derivative_compose Transcendental.DERIV_exp)
+    by (simp add: has_derivative_compose)
   have ** : "DERIV id x :> 1"
     by (metis DERIV_ident eq_id_iff)
   have *** : "DERIV h x :> x * (- (exp (- x))) + 1 * (exp (- x))"
-    by (simp add: * ** has_derivative_mult)
+    by (simp add: * ** has_derivative_mult comp_def)
   show ?thesis
     by (metis "***" left_diff_distrib mult_minus_right uminus_add_conv_diff)
 qed
 
 
+lemma q2_b : "0 \<le> x \<and> x \<le> y \<and> y \<le> 1 \<Longrightarrow> h x \<le> h y"
+  sorry
+
+
+lemma q2_c : "1 \<le> x \<and> x \<le> y \<Longrightarrow> h x \<ge> h y"
+  sorry
+
+
+subsubsection*[q3a::Task, Task.concerns= "{examiner,validator,student}",
+level="oneStar", mark="1::int", type="formal"] 
+{* Vérifier que pour tout nombre réel x appartenant à l'intervalle [0..+\<infinity>], on a :
+   @term{h x = (exp (- x)) - (h' x)} *}
+
+lemma q3a : "h x = (exp (- x)) - (h' x)"
+  by (simp add : h_def h'_def left_diff_distrib)
+
+
+text*[a3a::Answer_Formal_Step]
+{* Fill in term and justification*}
+
+
 close_monitor*[exam] 
 
 end