API tools faq
paste
Advertisement
Guest User

Got so far

a guest
Sep 25th, 2022
67
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 15.85 KB | None | 0 0
raw download clone embed print report
  1. From Coq Require Import Arith.
  2. From Coq Require Import Wf_nat.
  3. From Coq Require Import ZArith.
  4. From Coq Require Import Peano_dec.
  5. From Coq Require Import ZArith_dec.
  6.  
  7. From Coqprime Require Import NatAux ZCAux ZCmisc ZSum Pmod Ppow.
  8.  
  9. (** * Compatibility lemmas (provisional) *)
  10.  
  11. (** more general than [NatAux] lemma *)
  12.  
  13. Definition CoPrime (a b : nat) := (* done *)
  14. Zis_gcd (Z.of_nat a) (Z.of_nat b) 1%Z.
  15.  
  16. Lemma coPrimeSym (* done *) : forall a b : nat, CoPrime a b -> CoPrime b a.
  17. Proof. intros. now apply Zis_gcd_sym. Qed.
  18.  
  19. Definition LinComb (c x y: Z) := exists a b: Z, c = x * a + y * b.
  20.  
  21. Lemma gcd_lincomb_nat:
  22. forall (x y d : nat),
  23. (x > 0)%nat ->
  24. Zis_gcd (Z_of_nat x) (Z_of_nat y) (Z_of_nat d) ->
  25. LinComb (Z_of_nat d) (Z_of_nat x) (Z_of_nat y).
  26. Proof.
  27. Admitted.
  28.  
  29. Lemma coPrimeMult : (* done *)
  30. forall a b c : nat, CoPrime a b -> divide a (b * c) -> divide a c.
  31. Proof.
  32. intros ? ? ? H H0; unfold CoPrime in H.
  33. induction a as [| a _].
  34. - (* a = 0 *)
  35. induction H0 as (x, H0).
  36. cbn in H0. rewrite Nat.eq_mul_0 in H0. (* b = O \/ c = O *)
  37. destruct H0 as [H1 | H1].
  38. + rewrite H1 in H. simpl in H.
  39. inversion H. clear H H0 H1 H2.
  40. assert (2 | 0). { exists 0. auto. }
  41. destruct (H3 _ H H). nia.
  42. + rewrite H1. exists 0%nat. auto.
  43. - assert (H1: (S a > 0)%nat) by apply gt_Sn_O.
  44. destruct (gcd_lincomb_nat _ _ 1 H1 H) as [x [x0 H2]].
  45. destruct H0 as [x1 H0].
  46. assert (1 * Z.of_nat c = Z_of_nat (S a) * (x * Z.of_nat c + Z.of_nat x1 * x0)).
  47. { rewrite (Z.mul_comm (Z.of_nat (S a))).
  48. rewrite Z.mul_add_distr_r.
  49. rewrite (Z.mul_comm (x * Z.of_nat c)).
  50. rewrite (Z.mul_comm (Z.of_nat x1 * x0)).
  51. repeat rewrite Z.mul_assoc.
  52. rewrite <- Znat.inj_mult.
  53. rewrite <- H0.
  54. rewrite Znat.inj_mult.
  55. rewrite (Z.mul_comm (Z.of_nat b)).
  56. rewrite <- (Z.mul_assoc (Z.of_nat c)).
  57. rewrite (Z.mul_comm (Z.of_nat c)).
  58. rewrite <- Z.mul_add_distr_r.
  59. now rewrite <- H2. }
  60. rewrite Zmult_1_l in H3.
  61. assert (Z.divide (Z.of_nat (S a)) (Z.of_nat c)).
  62. { exists (x * Z.of_nat c + Z.of_nat x1 * x0).
  63. now rewrite Z.mul_comm at 1. }
  64. clear H2 H3 x x0.
  65. rewrite <- (Znat.Zabs2Nat.id (S a)).
  66. rewrite <- (Znat.Zabs2Nat.id c).
  67. repeat rewrite Zabs2Nat.id. destruct H4. exists (Z.to_nat x). lia.
  68. Qed.
  69.  
  70. Lemma coPrimeMult2 : (* done *)
  71. forall a b c : nat,
  72. CoPrime a b -> divide a c -> divide b c -> divide (a * b) c.
  73. Proof.
  74. intros a b c H H0 [x H1].
  75. assert (divide a x).
  76. { eapply coPrimeMult with (1:= H); now rewrite <- H1. }
  77. destruct H2 as [x0 H2]; exists x0; subst; ring.
  78. Qed.
  79.  
  80. Lemma ltgt1 (* done *): forall a b : nat, (a < b -> b > 0)%nat. (* done *)
  81. Proof. lia. Qed.
  82.  
  83. Lemma minus1 (* done *) : forall a b c : Z, (a - c)%Z = (b - c)%Z -> a = b.
  84. Proof. lia. Qed.
  85.  
  86. Lemma chRem2 : (* done *)
  87. forall b1 r1 b2 r2 q : Z,
  88. (0 <= r1)%Z ->
  89. (0 <= r2)%Z ->
  90. (r1 < q)%Z -> (r2 < q)%Z -> (b1 * q + r1)%Z = (b2 * q + r2)%Z ->
  91. r1 = r2.
  92. Proof.
  93. intros * H H0 H1 H2 H3.
  94. assert (H4: ((b1 - b2) * q)%Z = (r2 - r1)%Z) by
  95. (rewrite Z.mul_sub_distr_r; lia).
  96. induction (Zle_or_lt 0 (b1 - b2)) as [H5 | H5].
  97. induction (Zle_lt_or_eq _ _ H5) as [H6 | H6].
  98. assert (H7: (1 <= b1 - b2)%Z).
  99. { replace 1%Z with (Z.succ 0).
  100. apply Zlt_le_succ.
  101. assumption.
  102. auto.
  103. }
  104. assert (H8:(q <= r2 - r1)%Z).
  105. { replace q with (1 * q)%Z.
  106. rewrite <- H4.
  107. apply Zmult_le_compat_r.
  108. assumption.
  109. eapply Z.le_trans.
  110. apply H.
  111. apply Zlt_le_weak.
  112. assumption.
  113. apply Zmult_1_l.
  114. }
  115. set (A1 := Zplus_lt_le_compat r2 q (- r1) 0 H2) in *.
  116. assert (H9:(r2 - r1 < q)%Z).
  117. { replace q with (q + 0)%Z.
  118. unfold Zminus in |- *.
  119. apply A1.
  120. eapply (fun a b : Z => Zplus_le_reg_l a b r1).
  121. rewrite Zplus_opp_r.
  122. rewrite <- Zplus_0_r_reverse.
  123. assumption.
  124. rewrite <- Zplus_0_r_reverse.
  125. reflexivity.
  126. }
  127. elim (Zle_not_lt q (r2 - r1)).
  128. assumption.
  129. assumption.
  130. rewrite <- H6 in H4.
  131. rewrite Z.mul_comm in H4.
  132. rewrite <- Zmult_0_r_reverse in H4.
  133. rewrite <- (Zplus_opp_r r2) in H4.
  134. unfold Zminus in H4.
  135. apply Z.opp_inj.
  136. symmetry in |- *.
  137. eapply Zplus_reg_l.
  138. apply H4.
  139. assert (H6:(1 <= b2 - b1)%Z).
  140. { replace 1%Z with (Z.succ 0).
  141. apply Zlt_le_succ.
  142. apply (Zplus_lt_reg_l 0 (b2 - b1) b1).
  143. rewrite Zplus_minus.
  144. rewrite <- Zplus_0_r_reverse.
  145. apply (Zplus_lt_reg_l b1 b2 (- b2)).
  146. rewrite Zplus_opp_l.
  147. rewrite Zplus_comm.
  148. unfold Zminus in H5.
  149. assumption.
  150. auto.
  151. }
  152. assert (H7: ((b2 - b1) * q)%Z = (r1 - r2)%Z) by
  153. ( rewrite Z.mul_sub_distr_r ; lia ).
  154. assert (H8:(q <= r1 - r2)%Z).
  155. { replace q with (1 * q)%Z.
  156. rewrite <- H7.
  157. apply Zmult_le_compat_r.
  158. assumption.
  159. eapply Z.le_trans.
  160. apply H.
  161. apply Zlt_le_weak.
  162. assumption.
  163. apply Zmult_1_l.
  164. }
  165. set (A1 := Zplus_lt_le_compat r1 q (- r2) 0 H1) in *.
  166. assert (H9:(r1 - r2 < q)%Z).
  167. { replace q with (q + 0)%Z.
  168. unfold Zminus in |- *.
  169. apply A1.
  170. eapply (fun a b : Z => Zplus_le_reg_l a b r2).
  171. rewrite Zplus_opp_r.
  172. rewrite <- Zplus_0_r_reverse.
  173. assumption.
  174. rewrite <- Zplus_0_r_reverse.
  175. reflexivity.
  176. }
  177. elim (Zle_not_lt q (r1 - r2)).
  178. assumption.
  179. assumption.
  180. Qed.
  181.  
  182.  
  183.  
  184. Open Scope nat_scope.
  185.  
  186. Lemma uniqueRem : (* done *)
  187. forall r1 r2 b : nat,
  188. b > 0 ->
  189. forall a : nat,
  190. (exists q : nat, a = q * b + r1 /\ b > r1) ->
  191. (exists q : nat, a = q * b + r2 /\ b > r2) -> r1 = r2.
  192. Proof.
  193. intros ? ? ? H a [x [H0 H2]] [x0 [H1 H3]].
  194. assert (x = x0). { nia. } nia.
  195. Qed.
  196.  
  197. Lemma modulo :
  198. forall b : nat, b > 0 ->
  199. forall a : nat, {p : nat * nat | a = fst p * b + snd p /\ b > snd p}.
  200. Proof.
  201. intros b H a; apply (gt_wf_rec a).
  202. intros n H0 .
  203. destruct (le_lt_dec b n) as [Hle | Hlt].
  204. - assert (n > n - b).
  205. { unfold gt in |- *; apply lt_minus; assumption. }
  206. destruct (H0 _ H1) as [[a1 b0] p].
  207. simpl in p; exists (S a1, b0); simpl in |- *.
  208. destruct p as (H2, H3).
  209. split.
  210. + rewrite <- Nat.add_assoc, <- H2.
  211. now apply le_plus_minus.
  212. + assumption.
  213. - exists (0, n); simpl in |- *; now split.
  214. Qed.
  215.  
  216.  
  217. Lemma chRem1 : (* done *)
  218. forall b : nat, b > 0 -> forall a : Z,
  219. {p : Z * nat | snd p < b /\
  220. Z.of_nat (snd p) = (fst p * Z.of_nat b + a)%Z}.
  221. Proof.
  222. intros b H a.
  223. assert
  224. (H0: forall a' : Z,
  225. (a' >= 0)%Z ->
  226. {p : Z * nat | snd p < b /\
  227. Z.of_nat (snd p) =
  228. (fst p * Z.of_nat b + a')%Z}).
  229. { intros a' H0; set (A := Z.to_nat a') in *.
  230. induction (modulo b H A) as [x p].
  231. destruct x as (a0, b0).
  232. exists ((- Z.of_nat a0)%Z, b0).
  233. destruct p as (H1, H2).
  234. split.
  235. - apply H2.
  236. - rewrite <- (Z2Nat.id a').
  237. + simpl fst ; simpl snd.
  238. rewrite Zopp_mult_distr_l_reverse.
  239. rewrite Z.add_comm.
  240. fold (Z.of_nat (Z.to_nat a') - Z.of_nat a0 * Z.of_nat b)%Z
  241. in |- *.
  242. apply Zplus_minus_eq.
  243. rewrite <- Znat.inj_mult.
  244. rewrite <- Znat.inj_plus.
  245. apply Znat.inj_eq.
  246. apply H1.
  247. + auto.
  248. now rewrite <- Z.ge_le_iff.
  249. }
  250. destruct (Z_ge_lt_dec a 0).
  251. + apply H0; assumption.
  252. + assert (a + Z.of_nat b * - a >= 0)%Z.
  253. induction b as [| b Hrecb].
  254. * elim (lt_irrefl _ H).
  255. * rewrite Znat.inj_S.
  256. rewrite Z.mul_comm.
  257. rewrite <- Zmult_succ_r_reverse.
  258. fold (- a * Z.of_nat b - a)%Z in |- *.
  259. rewrite Zplus_minus.
  260. replace 0%Z with (0 * Z.of_nat b)%Z.
  261. apply Zmult_ge_compat_r.
  262. rewrite (Zminus_diag_reverse a).
  263. rewrite <- (Zplus_0_l (- a)).
  264. unfold Zminus in |- *.
  265. apply Z.le_ge.
  266. apply Zplus_le_compat_r.
  267. apply Zlt_le_weak.
  268. assumption.
  269. replace 0%Z with (Z.of_nat 0).
  270. apply Znat.inj_ge.
  271. unfold ge in |- *.
  272. apply le_O_n.
  273. auto.
  274. auto.
  275. * induction (H0 _ H1) as [x [H2 H3]].
  276. induction x as (a0, b1).
  277. exists ((a0 - a)%Z, b1).
  278. split.
  279. -- simpl in |- *; apply H2.
  280. -- cbv beta iota zeta delta [fst snd] in |- *.
  281. cbv beta iota zeta delta [fst snd] in H3.
  282. rewrite H3.
  283. rewrite (Zplus_comm a).
  284. rewrite Zplus_assoc.
  285. apply Zplus_eq_compat.
  286. rewrite Zmult_minus_distr_r.
  287. unfold Zminus in |- *.
  288. apply Zplus_eq_compat.
  289. reflexivity.
  290. rewrite Z.mul_comm.
  291. apply Zopp_mult_distr_l_reverse.
  292. reflexivity.
  293. Qed.
  294.  
  295. Lemma euclid_gcd1 :
  296. forall (d : nat) (x y q r : Z), Zis_gcd x y (Z.of_nat d) -> x = (q * y + r)%Z -> Zis_gcd r y (Z.of_nat d).
  297. Proof.
  298. intros. rewrite H0 in H. clear H0 x.
  299. replace (q * y + r)%Z with (r - (- q) * y)%Z in H by lia.
  300. apply Zis_gcd_sym in H. apply Zis_gcd_for_euclid in H. auto.
  301. Qed.
  302.  
  303. Lemma euclid_gcd :
  304. forall (d1 d2 : nat) (x y q r : Z),
  305. x = (q * y + r)%Z -> Zis_gcd x y (Z.of_nat d1) -> Zis_gcd r y (Z.of_nat d2) -> d1 = d2.
  306. Proof.
  307. intros. pose proof (euclid_gcd1 d1 x y q r H0 H).
  308. pose proof (Zis_gcd_unique r y _ _ H2 H1). lia.
  309. Qed.
  310.  
  311. Lemma gcd_lincomb_nat_dec :
  312. forall x y d : nat,
  313. x > 0 ->
  314. Zis_gcd (Z.of_nat x) (Z.of_nat y) (Z.of_nat d) ->
  315. {a : Z * Z |
  316. Z.of_nat d = (Z.of_nat x * fst a + Z.of_nat y * snd a)%Z}.
  317. Proof.
  318. intro x; apply (lt_wf_rec x); intros X IH. intros y d H H0.
  319. elim (modulo X H y).
  320. intro z; elim z.
  321. intros q r; clear z; simpl in |- *.
  322. case r.
  323. (* case r = 0 *)
  324. - intros; induction p as (H1, H2).
  325. rewrite <- plus_n_O in H1.
  326. exists (1%Z, 0%Z).
  327. simpl fst; simpl snd.
  328. rewrite <- Zmult_0_r_reverse; rewrite <- Zplus_0_r_reverse.
  329. rewrite Z.mul_comm. rewrite Zmult_1_l.
  330. apply Znat.inj_eq.
  331. apply (euclid_gcd d X (Z.of_nat y) (Z.of_nat X) (Z.of_nat q) 0).
  332. rewrite <- Zplus_0_r_reverse; rewrite <- Znat.inj_mult;
  333. apply Znat.inj_eq; assumption.
  334. apply Zis_gcd_sym; assumption.
  335. constructor.
  336. + exists 0%Z. auto.
  337. + exists 1%Z. lia.
  338. + auto.
  339. - (* case r > 0 *)
  340. intros r1 [H1 H2].
  341. elim (IH (S r1) H2 X d).
  342. + intro z; elim z.
  343. intros delta gamma; clear z.
  344. simpl fst; simpl snd.
  345. intros p.
  346. exists ((gamma - Z.of_nat q * delta)%Z, delta).
  347. simpl fst; simpl snd.
  348. rewrite p, H1.
  349. unfold Zminus in |- *; rewrite Zmult_plus_distr_r.
  350. rewrite Znat.inj_plus; rewrite Zmult_plus_distr_l.
  351. rewrite Znat.inj_mult; rewrite <- Zopp_mult_distr_l_reverse.
  352. rewrite (Z.mul_assoc (Z.of_nat X)).
  353. rewrite (Z.mul_comm (Z.of_nat X) (- Z.of_nat q)).
  354. rewrite Zopp_mult_distr_l_reverse.
  355. rewrite Zopp_mult_distr_l_reverse.
  356. rewrite <- (Z.add_assoc (Z.of_nat X * gamma)).
  357. rewrite <- Znat.inj_mult.
  358. rewrite (Z.add_assoc (- (Z.of_nat (q * X) * delta))).
  359. rewrite Zplus_opp_l. simpl in |- *. apply Z.add_comm.
  360. + auto with arith.
  361. + apply (euclid_gcd1 d (Z.of_nat y) (Z.of_nat X) (Z.of_nat q) (Z.of_nat (S r1))).
  362. * apply Zis_gcd_sym; assumption.
  363. * rewrite <- Znat.inj_mult; rewrite <- Znat.inj_plus;
  364. apply Znat.inj_eq; assumption.
  365. Qed.
  366.  
  367. Lemma chineseRemainderTheoremHelp :
  368. forall x1 x2 : nat,
  369. CoPrime x1 x2 ->
  370. forall (a b : nat) (pa : a < x1) (pb : b < x2),
  371. a <= b ->
  372. {y : nat |
  373. y < x1 * x2 /\
  374. a = snd (proj1_sig (modulo x1 (ltgt1 _ _ pa) y)) /\
  375. b = snd (proj1_sig (modulo x2 (ltgt1 _ _ pb) y))}.
  376. Proof.
  377. intros ? ? H a b pa pb H0. unfold CoPrime in H.
  378. replace 1%Z with (Z.of_nat 1) in H by auto.
  379. destruct (gcd_lincomb_nat_dec _ _ _ (ltgt1 _ _ pa) H)
  380. as [(a0,b0) p].
  381. set (A := Z.of_nat a) in *.
  382. set (B := Z.of_nat b) in *.
  383. set (X1 := Z.of_nat x1) in *.
  384. set (X2 := Z.of_nat x2) in *.
  385. set (y := (a0 * (B - A))%Z) in *.
  386. set (z := (b0 * (A - B))%Z) in *.
  387. set (d := (A + X1 * y)%Z) in *.
  388. assert (d = (B + X2 * z)%Z).
  389. unfold d in |- *; simpl in p.
  390. apply minus1 with (X2 * z)%Z.
  391. rewrite (Z.add_comm B).
  392. rewrite Zminus_plus.
  393. unfold z in |- *.
  394. replace (A - B)%Z with (- (B - A))%Z.
  395. unfold Zminus in |- *.
  396. rewrite (Z.mul_comm b0).
  397. rewrite Zopp_mult_distr_l_reverse.
  398. rewrite (Z.mul_comm X2).
  399. rewrite Zopp_mult_distr_l_reverse.
  400. rewrite Z.opp_involutive.
  401. unfold y in |- *.
  402. rewrite <- (Z.mul_assoc (B + - A)).
  403. rewrite (Z.mul_comm (B + - A)).
  404. rewrite (Z.mul_assoc X1).
  405. rewrite (Z.mul_comm b0).
  406. rewrite <- Z.add_assoc.
  407. rewrite <- Zmult_plus_distr_l.
  408. rewrite <- p.
  409. rewrite Z.mul_1_l.
  410. fold (B - A)%Z in |- *.
  411. apply Zplus_minus.
  412. unfold Zminus in |- *.
  413. rewrite Zopp_plus_distr.
  414. rewrite Z.add_comm.
  415. rewrite Z.opp_involutive.
  416. reflexivity.
  417. assert (H2: x1 * x2 > 0).
  418. replace 0 with (0 * x2).
  419. unfold gt in |- *.
  420. rewrite Nat.mul_comm.
  421. rewrite (Nat.mul_comm x1).
  422. induction x2 as [| x2 Hrecx2].
  423. elim (lt_n_O _ pb).
  424. apply mult_S_lt_compat_l.
  425. fold (x1 > 0) in |- *.
  426. eapply ltgt1.
  427. apply pa.
  428. auto.
  429. destruct (chRem1 _ H2 d) as [(a1, b1) [H3 H4]].
  430. exists b1; split.
  431. apply H3.
  432. cbv beta iota zeta delta [snd fst] in H4, p.
  433. split.
  434. induction (modulo x1 (ltgt1 a x1 pa) b1).
  435. induction x as (a2, b2).
  436. simpl in |- *.
  437. induction p0 as (H5, H6).
  438. cbv beta iota zeta delta [snd fst] in H5.
  439. rewrite H5 in H4.
  440. unfold d in H4.
  441. unfold A, X1 in H4.
  442. assert (Z.of_nat a = Z.of_nat b2).
  443. { eapply chRem2; try lia.
  444. + apply Znat.inj_lt.
  445. apply pa.
  446. + apply Znat.inj_lt.
  447. apply H6.
  448. + rewrite Znat.inj_plus in H4.
  449. repeat rewrite Znat.inj_mult in H4.
  450. symmetry in |- *.
  451. rewrite (Z.add_comm (Z.of_nat a)) in H4.
  452. rewrite Z.add_assoc in H4.
  453. rewrite Z.mul_assoc in H4.
  454. rewrite (Z.mul_comm a1) in H4.
  455. rewrite <- (Z.mul_assoc (Z.of_nat x1)) in H4.
  456. rewrite <- Zmult_plus_distr_r in H4.
  457. rewrite (Z.mul_comm (Z.of_nat x1)) in H4.
  458. apply H4. }
  459. lia.
  460. induction (modulo x2 (ltgt1 b x2 pb) b1).
  461. simpl in |- *.
  462. induction x as (a2, b2).
  463. cbv beta iota zeta delta [snd fst] in p0.
  464. induction p0 as (H5, H6).
  465. rewrite H5 in H4.
  466. rewrite H1 in H4.
  467. unfold B, X2 in H4.
  468. simpl. assert (Z.of_nat b = Z.of_nat b2).
  469. { eapply chRem2; try lia.
  470. + apply Znat.inj_lt.
  471. apply pb.
  472. + apply Znat.inj_lt.
  473. apply H6.
  474. + rewrite Znat.inj_plus in H4.
  475. repeat rewrite Znat.inj_mult in H4.
  476. symmetry in |- *.
  477. rewrite (Z.add_comm (Z.of_nat b)) in H4.
  478. rewrite Z.mul_assoc in H4.
  479. rewrite Z.add_assoc in H4.
  480. rewrite (Z.mul_comm a1) in H4.
  481. rewrite (Z.mul_comm (Z.of_nat x2)) in H4.
  482. rewrite <- Zmult_plus_distr_l in H4.
  483. apply H4. }
  484. lia.
  485. Qed.
  486.  
  487. Lemma chineseRemainderTheorem :
  488. forall x1 x2 : nat,
  489. CoPrime x1 x2 ->
  490. forall (a b : nat) (pa : a < x1) (pb : b < x2),
  491. {y : nat |
  492. y < x1 * x2 /\
  493. a = snd (proj1_sig (modulo x1 (ltgt1 _ _ pa) y)) /\
  494. b = snd (proj1_sig (modulo x2 (ltgt1 _ _ pb) y))}.
  495. Proof.
  496. intros ? ? H a b pa pb.
  497. destruct (le_lt_dec a b).
  498. - apply chineseRemainderTheoremHelp; assumption.
  499. - assert (H0: b <= a) by (now apply lt_le_weak).
  500. assert (H1: CoPrime x2 x1) by (now apply coPrimeSym).
  501. induction (chineseRemainderTheoremHelp _ _ H1 b a pb pa H0)
  502. as [x [H2 [H3 H4]]].
  503. exists x.
  504. split.
  505. + now rewrite Nat.mul_comm.
  506. + split; assumption.
  507. Qed.
  508.  
  509. Fixpoint prod (n:nat) (x: nat -> nat) :=
  510. match n with
  511. O => 1%nat
  512. | S p => x p * prod p x
  513. end.
  514.  
  515. Definition factorial (n : nat) : nat := prod n S.
  516.  
  517. Lemma coPrime1 : forall a : nat, CoPrime 1 a.
  518. Proof.
  519. split.
  520. - simpl. exists 1%Z. auto.
  521. - exists (Z.of_nat a); lia.
  522. - intros e [H H0] [H1 H2].
  523. simpl in H0. symmetry in H0.
  524. assert (H >= 0 \/ H <= 0)%Z by lia. destruct H3.
  525. + pose proof (Zmult_one _ _ H3 H0). subst. exists 1%Z. lia.
  526. + assert (- H >= 0)%Z by lia.
  527. replace (H * e)%Z with ((- H) * (- e))%Z in H0 by lia.
  528. pose proof (Zmult_one _ _ H4 H0). rewrite H5 in H0.
  529. exists (-1)%Z. lia.
  530. Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!