diff --git a/smc/smc_entropy.v b/smc/smc_entropy.v
index c96977ba..49919765 100644
--- a/smc/smc_entropy.v
+++ b/smc/smc_entropy.v
@@ -8,11 +8,39 @@ Require Import proba jfdist_cond entropy graphoid smc_proba.
 Import GRing.Theory.
 Import Num.Theory.
 
-(******************************************************************************)
-(*                              SMC Proofs in entroy                          *)
-(*     From: Information-theoretically Secure Number-product Protocol         *)
-(*                                                                            *)
-(******************************************************************************)
+(************************************************************************************)
+(*                              SMC Proofs in entroy                                *)
+(*                                                                                  *)
+(*     From: Information-theoretically Secure Number-product Protocol               *)
+(*     SHEN, Chih-Hao, et al. In: 2007 International Conference on Machine          *)
+(*     Learning and Cybernetics. IEEE, 2007. p. 3006-3011.                          *)
+(*                                                                                  *)
+(*                                                                                  *)
+(* |   Definitions     |    | Meaning                                              |*)
+(* |-------------------|----|------------------------------------------------------|*)
+(* |    x \*d y        | == | dot product of two random vectors.                   |*)
+(* | scalar_product    | == | The deterministic version of                         |*)
+(* |                   |    | SMC scalar product protocol as a function.           |*)
+(* | is_scalar_product | == | The correctness of the SMC scalar product results    |*)
+(* |-------------------------------------------------------------------------------|*)
+(*                                                                                  *)
+(*                                                                                  *)
+(* Lemmas:                                                                          *)
+(*   pi2_bob_is_leakage_free_proof   == the proof shows that Bob's knowledge of     *)
+(*                                      Alice's secret input x1 does not increase   *)
+(*                                      by accessing random variables received      *)
+(*                                      during the protocols execution              *)
+(*   pi2_alice_is_leakage_free_proof == the proof shows that Alice's knowledge of   *)
+(*                                      Bob's secret input x2 does not increase     *)
+(*                                      by accessing random variables received      *)
+(*                                      during the protocols execution              *)
+(*   cpr_cond_entropy                == given a conditional probability removal     *)
+(*                                      lemma P( X | (Y, Z))->P( X | Y ), shows that*)
+(*                                      with some conditions met, there exists a    *)
+(*                                      conditional entropy removal lemma           *)
+(*                                      H( X | (Y, Z))->H( X | Y )                  *)
+(*                                                                                  *)
+(************************************************************************************)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/smc/smc_interpreter.v b/smc/smc_interpreter.v
index e6304fe9..27e8aa69 100644
--- a/smc/smc_interpreter.v
+++ b/smc/smc_interpreter.v
@@ -453,9 +453,11 @@ Qed.
 Let x1x2s2x1'r2_y2_indepP :=
   x1x2s2x1'r2_y2_indep (x2s2x1s1r2_y2_indep (x2s2x1s1r1_y2_indep inputs)).
 
+
 Let x2s2x1s1_r2_indep :
   P |= [% x2, s2, x1, s1] _|_ [%s1, s2, r1].
 Proof.
+
 rewrite inde_rv_events'.
 rewrite /inde_rv_ev => E F.
 rewrite (reasoning_by_cases [%s1, s2, r1] [% x2, s2, x1, s1]).
diff --git a/smc/smc_proba.v b/smc/smc_proba.v
index 1c14e7a8..25d2445f 100644
--- a/smc/smc_proba.v
+++ b/smc/smc_proba.v
@@ -11,11 +11,15 @@ Require Import proba jfdist_cond graphoid.
 Import GRing.Theory.
 Import Num.Theory.
 
-(******************************************************************************)
-(*                              SMC Useful Tools                              *)
-(*     From: Information-theoretically Secure Number-product Protocol         *)
-(*                                                                            *)
-(******************************************************************************)
+(************************************************************************************)
+(*                              SMC "Useful Tools" probability lemmas               *)
+(*                                                                                  *)
+(*     From: Information-theoretically Secure Number-product Protocol,              *)
+(*           Sec. III.B  "Useful Tools"                                             *)
+(*     SHEN, Chih-Hao, et al. In: 2007 International Conference on Machine          *)
+(*     Learning and Cybernetics. IEEE, 2007. p. 3006-3011.                          *)
+(*                                                                                  *)
+(************************************************************************************)
 
 Set Implicit Arguments.
 Unset Strict Implicit.