#include <iostream>
using namespace std;
int main(){
cout<<"This is cpp code block"<<"\n";
return 0;
}
Theorem inversion_on_constr: forall n m: nat, S n = S m -> n = m.
Proof.
intros n m H.
inversion H.
reflexivity.
Qed.
$$\KaTeX$$ Now Available
$$|\vec{F_E}| =\frac{1}{4\pi\epsilon}|\frac{q_1q_2}{r^2}|$$
$$\vec E=\frac{\vec F_E}{q}$$
$$\phi=\oint\vec{E}\cdot d\vec{A}=\frac{Q}{\epsilon_0}$$
$$E_x=-\frac{dV}{dx}$$ ($V$ is decreasing)
$$\frac{d}{dx}tan x=sec^2x$$
