-lemma O_refl: ∀s. O s s.
-#s %{1} %{0} #n #_ >commutative_times <times_n_1 @le_n qed.
-
-lemma O_trans: ∀s1,s2,s3. O s2 s1 → O s3 s2 → O s3 s1.
-#s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1*c2)}
-%{(max n1 n2)} #n #Hmax
-@(transitive_le … (H1 ??)) [@(le_maxl … Hmax)]
->associative_times @le_times [//|@H2 @(le_maxr … Hmax)]
+lemma O_refl: ∀s. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s s.
+#s %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6} %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6} #n #_ >\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/times_n_1.def(8)"\ 6times_n_1\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 qed.
+
+lemma O_trans: ∀s1,s2,s3. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 s1 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s3 s2 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s3 s1.
+#s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c2)}
+%{(\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n1 n2)} #n #Hmax
+@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … (H1 ??)) [@(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … Hmax)]
+>\ 5a href="cic:/matita/arithmetics/nat/associative_times.def(10)"\ 6associative_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 [//|@H2 @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … Hmax)]