sayon/coq-am-gm

an attempt to formalize arithmetic mean >= geometric

coq-am-gm

Formalization of the inequality of arithmetic and geometric means for natural numbers using Coq proof assistant, extended with SSReflect.

http://en.wikipedia.org/wiki/Inequality_of_arithmetic_and_geometric_means