Now pervasive in many mathematics and computer science research domains, proof assistants have recently gained importance in education, mostly during the college years. In this article, we propose a new learning environment as a layer above the Lean proof assistant, specifically targeting high-school level proofs. Drawing inspiration from coherent logic and adaptations of proof assistants for teaching, such as Lean-Verbose and Coq Waterproof, along with our own experience using proof assistants in higher education, we designed Yalep , a declarative controlled natural language, with a minimal number of syntactic constructions, which favors forward-chaining of facts. Yalep provides convenience for type theory hiding, and functions defined on type subsets. This paper presents the design choices and implementation of these features.