Justifying and prooving in the cabri environment