proposition: Lemma conditional_rewrite_example : forall n:nat, 8 <= n + 6 -> 3 + n < 6 -> n * n = n + n.
proof: Proof. intros n H H0. rewrite <- (le_lt_S_eq 2 n). - reflexivity. - apply Nat.add_le_mono_l with (p := 6). rewrite Nat.add_comm in H; auto with arith. - apply Nat.add_lt_mono_l with (p:= 3); auto with arith. Qed.
imports: ZArith List Arith ZArithRing Relations Lia