proposition: Lemma div_not_qlt : forall (a b : nat) (q q' r r' : nat), a = q * b + r -> a = q' * b + r' -> b > r -> b > r' -> ~ q < q'.
proof: Proof. intros a b q q' r r' Hdiv Hdiv' Hrem Hrem' Hqlt. assert (Hle: b <= r). { - apply le_trans with (r - r'). + rewrite <- Nat.mul_1_l with b. replace (r - r') with ((q' - q) * b). * apply mul_le_mono_r; abstract lia. * transitivity (q' * b - q * b). { apply Nat.mul_sub_distr_r. } symmetry; apply Nat.add_sub_eq_l. rewrite minus_semi_assoc with r' (q' * b) (q * b). apply Nat.add_sub_eq_l. transitivity a. now symmetry. { now rewrite Nat.add_comm with r' (q' * b). } unfold gt; apply Nat.mul_lt_mono_pos_r. lia. assumption. + apply Nat.le_sub_l. } rewrite (Nat.lt_nge r b ) in Hrem; contradiction. Qed.
imports: Coq(Arith Lia )