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.