<div dir="ltr"><div>Since now, I have spent days proving trivial mathematical propositions without knowing if the general theory/idea is correct.</div><div><br></div><div>This, of course, means that the theory is developed while programming in Agda. It is not developed before using Agda.</div><div><br></div><div>I am thinking of using postulates extensively and prove things on paper instead of doing it in Agda.</div><div>It is less safe but much faster. Then check the validity of the main Idea with the use of the postulates. Only then try to prove some of the postulates that might be a bit tricky.</div><div><br></div><div>At least for me, proofs that do not take part in the computation of a program can remain postulates.</div><div><br></div><div>What is your strategy? Do you use postulates extensively? In my opinion this is important enough that it needs to be put in the documentation. I have wasted too much time proving trivial propositions and we do not have to do that.<br></div></div>