This commit is contained in:
Thomas Baruchel 2023-01-27 17:39:07 +01:00
parent 4b5ab5a9c6
commit 63284a1542

View File

@ -1833,7 +1833,22 @@ Proof.
apply Nat.le_refl.
Admitted.
rewrite <- Nat.div_add. rewrite Nat.mul_comm.
replace (2 * Nat.div2 (length a'))
with (2 * Nat.div2 (length a') + Nat.b2n (Nat.odd (length a'))).
rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity.
rewrite <- Nat.negb_even. rewrite J'. simpl. rewrite Nat.add_0_r.
reflexivity. easy. easy. rewrite Nat.div2_div. reflexivity.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
apply Nat.le_refl.
rewrite <- Nat.div_add. rewrite Nat.mul_comm.
replace (2 * Nat.div2 (length a))
with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))).
rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity.
rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r.
reflexivity. easy.
Qed.