diff --git a/examples/programs/fibonacci.mlw b/examples/programs/fibonacci.mlw
index 97cc7408531a0a6b5d64823b49c565a7d84e1f59..97f5ce45677fde837f18ee30212df5a0c605ab07 100644
--- a/examples/programs/fibonacci.mlw
+++ b/examples/programs/fibonacci.mlw
@@ -86,6 +86,11 @@ module FibonacciLogarithmic
   logic m1110 : t = {| a11 = 1; a12 = 1;
                        a21 = 1; a22 = 0 |}
 
+  (* computes ((1 1) (1 0))^n in O(log(n)) time
+
+     since it is a matrix of the shape ((a+b b) (b a)), 
+     we only return the pair (a, b) *)
+
   let rec logfib n =
     { n >= 0 }
     if n = 0 then 
@@ -101,6 +106,14 @@ module FibonacciLogarithmic
     { let a, b = result in 
       power m1110 n = {| a11 = a+b; a12 = b; a21 = b; a22 = a |} }
 
+  (* by induction, we easily prove that
+
+     (1 1)^n = (F(n+1) F(n)  )
+     (1 0)     (F(n)   F(n-1))
+
+    thus, we can compute F(n) in O(log(n)) using funtion logfib above
+  *)
+
   logic p (n:int) = 
     let p = power m1110 n in
     isfib (n+1) p.a11 and isfib n p.a21