transcript: improved debuugging facilities

[helm.git] / helm / software / matita / contribs / procedural / Coq / Reals / Rprod.mma

diff --git a/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma b/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma
index b85e455907148ed1daa2083fff6048f79e4380f0..db3a0a34ea9395d19d24d4a8bc4d7bda8e819827 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma
@@ -70,7 +70,7 @@ inline procedural "cic:/Coq/Reals/Rprod/fact_prodSO.con" as lemma.
 
 inline procedural "cic:/Coq/Reals/Rprod/le_n_2n.con" as lemma.
 
-(* We prove that (N!)²<=(2N-k)!*k! forall k in [|O;2N|] *)
+(* We prove that (N!)\178\<=(2N-k)!*k! forall k in [|O;2N|] *)
 
 inline procedural "cic:/Coq/Reals/Rprod/RfactN_fact2N_factk.con" as lemma.