- use the syntax of the driver for the own realization of a theory
 - add a *_def lemma for defined logics with syntax
 - add comments that inform which syntax is used for declared logic

Remark about the theory: if one considers that the square root is always
nonnegative (by definition in Coq), then Lemma Sqrt_positive has an
extraneous hypothesis.