proposition: Lemma divide_lcm_eq_r : forall n m, (n|m) -> lcm n m == m.
proof: Proof. intros n m H. apply lcm_unique_alt; trivial using le_0_l. intros q. split. - split; trivial. now transitivity m. - now destruct 1. Qed.
imports: NAxioms NSub NDiv NGcd