First, while you can express those statements in programming languages, they will either be expressed differently in order to have the same meaning or, if expressed in a similar way, have a different meaning (even ignoring that many such statements are not computable at all). This merely shows that math is not an FP language.
Second, you can prove those equivalences in any language that allows you to directly express relations, be it the type-level language of Agda, Coq or F*, or the contract language of an imperative language -- this is nothing to do with FP, but with a language that can express relations.
Second, you can prove those equivalences in any language that allows you to directly express relations, be it the type-level language of Agda, Coq or F*, or the contract language of an imperative language -- this is nothing to do with FP, but with a language that can express relations.