proposition: Lemma continuous2_sym (f:fterm2) : (forall x y, realp x -> realp y -> f x y = f y x) -> (forall x y, realp x -> realp y -> continuous_at (f x) y) -> continuous2 f.
proof: Proof. move => Ha Hb. move => x y xr yr; split; first by apply: Hb. move => e ep; move:(Hb _ _ yr xr) => h; move:(h _ ep) => [d da db]; ex_tac. move => t ta; move:(db _ ta). move: (ta) => [tr _]. by rewrite /BR_near (Ha _ _ yr tr)(Ha _ _ yr xr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)