n m (d : (n | m)) (gt0 : 0 < m) : 0 < n. Proof. destruct d as [d H]. destruct H. destruct (nat_zero_or_gt_zero n) as [z | s]. 2: exact s. destruct z; cbn in gt0. rewrite nat_mul_zero_r in gt0. exact gt0. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes