subeq-trans; way easier when casesplit on q first