File: bug_2145.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (19 lines) | stat: -rw-r--r-- 411 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
 
(* Test robustness of Groebner tactic in presence of disequalities *)

Require Export Reals.
Require Export Nsatz.

Open Scope R_scope.

Lemma essai :
 forall yb xb m1 m2 xa ya,
  xa <> xb ->
 yb - 2 * m2 * xb = ya - m2 * xa ->
 yb - m1 * xb = ya - m1 * xa ->
 yb - ya = (2 * xb - xa) * m2 ->
 yb - ya = (xb - xa) * m1.
Proof.
intros.
(* clear H. groebner used not to work when H was not cleared *)
nsatz.
Qed.