aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_047.v
blob: 29496be5eeff856ce23d5d1f5f3041ee2bb44fff (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
Inductive nCk : nat -> nat -> Type :=
  |zz : nCk 0 0
  | incl { m n : nat } : nCk m n -> nCk (S m) (S n)
  | excl { m n : nat } : nCk m n -> nCk (S m) n.

Definition nCkComp { l m n : nat } :
  nCk l m -> nCk m n -> nCk l n.
Proof.
  intro.
  revert n.
  induction H.
  auto.
(* ( incl w ) o zz -> contradiction *)
  intros.
    remember (S n) as sn.
    destruct H0.
      discriminate Heqsn.
    apply incl.
      apply IHnCk.
      injection Heqsn.
      intro.
      rewrite <- H1.
      auto.
    apply excl.
      apply IHnCk.
      injection Heqsn.
      intro. rewrite <- H1.
      auto.
  intros.
  apply excl.
  apply IHnCk.
  auto.
Defined.

Lemma nCkEq { k l m n : nat } ( cs : nCk k l ) (ct : nCk l m) (cr : nCk m n ):
  nCkComp cs (nCkComp ct cr) = nCkComp (nCkComp cs ct) cr.
Proof.
  revert m n ct cr.
  induction cs.
  intros. simpl. auto.
  intros.
  destruct n.
   destruct m0.
    destruct n0.
     destruct cr.
(* Anomaly: Evar ?nnn was not declared. Please report. *)